chore: rw? uses MVarId.refl not MVarId.applyRfl

leanprover · Mar 27, 2024 · a8784a9 · a8784a9
1 parent 80d2455
commit a8784a9
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/src/Lean/Meta/Tactic/Rewrites.lean b/src/Lean/Meta/Tactic/Rewrites.lean
@@ -7,7 +7,7 @@ prelude
 import Lean.Meta.LazyDiscrTree
 import Lean.Meta.Tactic.Assumption
 import Lean.Meta.Tactic.Rewrite
-import Lean.Meta.Tactic.Rfl
+import Lean.Meta.Tactic.Refl
 import Lean.Meta.Tactic.SolveByElim
 import Lean.Meta.Tactic.TryThis
 import Lean.Util.Heartbeats
@@ -140,7 +140,7 @@ def computeRfl (mctx : MetavarContext) (res : Meta.RewriteResult) : MetaM Bool :
   try
     withoutModifyingState <| withMCtx mctx do
       -- We use `withReducible` here to follow the behaviour of `rw`.
-      withReducible (← mkFreshExprMVar res.eNew).mvarId!.applyRfl
+      withReducible (← mkFreshExprMVar res.eNew).mvarId!.refl
       -- We do not need to record the updated `MetavarContext` here.
       pure true
   catch _e =>
@@ -168,7 +168,7 @@ def solveByElim (goals : List MVarId) (depth : Nat := 6) : MetaM PUnit := do
   let [] ← SolveByElim.solveByElim cfg lemmas ctx goals
     | failure
 
-def rwLemma (ctx : MetavarContext) (goal : MVarId) (target : Expr) (side : SideConditions := .solveByElim) 
+def rwLemma (ctx : MetavarContext) (goal : MVarId) (target : Expr) (side : SideConditions := .solveByElim)
     (lem : Expr ⊕ Name) (symm : Bool) (weight : Nat) : MetaM (Option RewriteResult) :=
   withMCtx ctx do
     let some expr ← (match lem with