add info

leanprover-community · Apr 12, 2023 · 37c0847 · 37c0847
1 parent 5c72719
commit 37c0847
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/Mathlib/Tactic/Eqns.lean b/Mathlib/Tactic/Eqns.lean
@@ -27,7 +27,7 @@ theorem transpose_const {m n} (c : ℕ) :
   rw [transpose]
 ```
 -/
-open Lean
+open Lean Elab
 
 syntax (name := eqns) "eqns" ident* : attr
 
@@ -37,7 +37,7 @@ initialize eqnsAttribute : NameMapExtension (Array Name) ←
     descr := "Overrides the equation lemmas for a declation to the provided list"
     add   :=  fun
     | _, `(attr| eqns $[$names]*) =>
-      names.mapM resolveGlobalConstNoOverload
+      names.mapM resolveGlobalConstNoOverloadWithInfo
     | _, _ => Lean.Elab.throwUnsupportedSyntax }
 
 initialize Lean.Meta.registerGetEqnsFn (fun name => do