chore: fix imports

leanprover-community · Sep 9, 2024 · 1af15aa · 1af15aa
1 parent 1a28ab0
commit 1af15aa
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/Batteries/CodeAction/Basic.lean b/Batteries/CodeAction/Basic.lean
@@ -6,6 +6,7 @@ Authors: Mario Carneiro
 import Lean.Elab.BuiltinTerm
 import Lean.Elab.BuiltinNotation
 import Lean.Server.InfoUtils
+import Lean.Server.CodeActions.Provider
 import Batteries.CodeAction.Attr
 
 /-!