From eb0e911c91293bc27aa29a442e9f70fdc8a00b66 Mon Sep 17 00:00:00 2001
From: Yan Peng <yppe@amazon.com>
Date: Wed, 20 Nov 2024 04:51:12 +0000
Subject: [PATCH] Fix an import issue

---
 Proofs/AES-GCM/GCMInitV8Sym.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Proofs/AES-GCM/GCMInitV8Sym.lean b/Proofs/AES-GCM/GCMInitV8Sym.lean
index 1a8d32c2..ad810490 100644
--- 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