move withRef

hhu-adam · Jun 17, 2024 · b5f9cb3 · b5f9cb3
1 parent 693dae1
commit b5f9cb3
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean
@@ -204,7 +204,7 @@ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (simprocs : Simp.SimprocsAr
                 arg[0][0].getKind == ``Parser.Tactic.simpPost
             let inv  := !arg[1].isNone
             let term := arg[2]
-            match (← withRef term do resolveSimpIdTheorem? term) with
+            match (← resolveSimpIdTheorem? term) with
             | .expr e  =>
               let name ← mkFreshId
               thms ← addDeclToUnfoldOrTheorem thms (.stx name arg) e post inv kind

diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
@@ -1769,7 +1769,7 @@ private def mkConsts (candidates : List (Name × List String)) (explicitLevels :
     return (const, projs) :: result
 
 def resolveName (stx : Syntax) (n : Name) (preresolved : List Syntax.Preresolved) (explicitLevels : List Level) (expectedType? : Option Expr := none) : TermElabM (List (Expr × List String)) := do
-  addCompletionInfo <| CompletionInfo.id stx stx.getId (danglingDot := false) (← getLCtx) expectedType?
+  withRef stx <| addCompletionInfo <| CompletionInfo.id stx stx.getId (danglingDot := false) (← getLCtx) expectedType?
   if let some (e, projs) ← resolveLocalName n then
     unless explicitLevels.isEmpty do
       throwError "invalid use of explicit universe parameters, '{e}' is a local"