Fix an import issue

pennyannn · Nov 20, 2024 · eb0e911 · eb0e911
1 parent e855c82
commit eb0e911
Showing 1 changed file with 0 additions and 1 deletion.
diff --git a/Proofs/AES-GCM/GCMInitV8Sym.lean b/Proofs/AES-GCM/GCMInitV8Sym.lean
@@ -8,7 +8,6 @@ import Proofs.«AES-GCM».GCMInitV8Pre
 import Tactics.Sym
 import Tactics.Aggregate
 import Specs.GCMV8
-import Tactics.ExtractGoal
 
 namespace GCMInitV8Program