chore: import Std.Data.HashMap in backported files

leanprover · Aug 29, 2024 · c122849 · c122849
1 parent d017635
commit c122849
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 0 deletions.
diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean
@@ -12,6 +12,7 @@ import Lean.Elab.Eval
 import Lean.Elab.Command
 import Lean.Elab.Open
 import Lean.Elab.SetOption
+import Std.Data.HashMap
 
 namespace Lean.Elab.Command
 

diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
@@ -16,6 +16,7 @@ import Lean.Elab.Deriving.Basic
 import Lean.Elab.PreDefinition.Main
 import Lean.Elab.PreDefinition.TerminationHint
 import Lean.Elab.DeclarationRange
+import Std.Data.HashMap
 
 namespace Lean.Elab
 open Lean.Parser.Term