.

leanprover · Oct 2, 2024 · 62f7e75 · 62f7e75
1 parent 66a5a95
commit 62f7e75
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/src/Lean/Meta/Tactic/Clear.lean b/src/Lean/Meta/Tactic/Clear.lean
@@ -61,8 +61,8 @@ appear in the local context.
 def _root_.Lean.MVarId.tryClearMany' (goal : MVarId) (fvarIds : Array FVarId) :
     MetaM (MVarId × Array FVarId) :=
   goal.withContext do
-    let hyps ← sortFVarsByContextOrder hyps
-    hyps.foldrM (init := (goal, Array.mkEmpty hyps.size))
+    let fvarIds ← sortFVarsByContextOrder fvarIds
+    fvarIds.foldrM (init := (goal, Array.mkEmpty fvarIds.size))
       fun h (goal, cleared) => do
         let goal' ← goal.tryClear h
         let cleared := if goal == goal' then cleared else cleared.push h