From 50fd39db8959b401d9e311378b69bd8e3a435c24 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 12 Mar 2021 17:48:33 -0800 Subject: [PATCH] fix: bug at `allGoals` --- src/Lean/Elab/Tactic/Basic.lean | 7 ++++--- tests/lean/run/allGoals.lean | 3 +++ 2 files changed, 7 insertions(+), 3 deletions(-) diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean index 51396dacc0..6ee14b499b 100644 --- a/src/Lean/Elab/Tactic/Basic.lean +++ b/src/Lean/Elab/Tactic/Basic.lean @@ -341,9 +341,10 @@ private def getOptRotation (stx : Syntax) : Nat := let gs ← getUnsolvedGoals let mut gsNew := [] for g in gs do - setGoals [g] - evalTactic stx[1] - gsNew := gsNew ++ (← getUnsolvedGoals) + unless ← isExprMVarAssigned g do + setGoals [g] + evalTactic stx[1] + gsNew := gsNew ++ (← getUnsolvedGoals) setGoals gsNew @[builtinTactic tacticSeq] def evalTacticSeq : Tactic := fun stx => diff --git a/tests/lean/run/allGoals.lean b/tests/lean/run/allGoals.lean index d457f98b35..886fadf7f9 100644 --- a/tests/lean/run/allGoals.lean +++ b/tests/lean/run/allGoals.lean @@ -58,3 +58,6 @@ theorem Weekday.test2 (d : Weekday) : next (previous d) = id d := by cases d <;> rw idEq traceState allGoals rfl + +def bug {a b c : Nat} (h₁ : a = b) (h₂ : b = c) : a = c := by + apply Eq.trans <;> assumption