From 39adda8ffeb01bbc46af3fa8322cb6b1997a501d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 2 Sep 2021 19:11:52 -0700 Subject: [PATCH] fix: missing goals --- src/Lean/Elab/Tactic/Conv/Rewrite.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Lean/Elab/Tactic/Conv/Rewrite.lean b/src/Lean/Elab/Tactic/Conv/Rewrite.lean index 009b10f408..9f8803b35c 100644 --- a/src/Lean/Elab/Tactic/Conv/Rewrite.lean +++ b/src/Lean/Elab/Tactic/Conv/Rewrite.lean @@ -16,6 +16,7 @@ def evalRewriteCore (mode : TransparencyMode) : Tactic := fun stx => let e ← elabTerm term none true let r ← rewrite (← getMainGoal) (← getLhs) e symm (mode := mode) updateLhs r.eNew r.eqProof + replaceMainGoal ((← getMainGoal) :: r.mvarIds) @[builtinTactic Lean.Parser.Tactic.Conv.rewrite] def evalRewrite : Tactic := evalRewriteCore TransparencyMode.instances