From eb036cc8aa569bb0b7c7e536f0b50ff2523c4a4c Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Thu, 8 Oct 2020 16:47:33 +0100
Subject: [PATCH] =?UTF-8?q?fix(init/meta/converter/interactive):=20Do=20no?=
 =?UTF-8?q?t=20allow=20rw=20to=20create=20=E2=8A=A2=20goals=20in=20conv=20?=
 =?UTF-8?q?mode?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 library/init/meta/converter/interactive.lean | 27 ++++++++++++--------
 1 file changed, 17 insertions(+), 10 deletions(-)

diff --git a/library/init/meta/converter/interactive.lean b/library/init/meta/converter/interactive.lean
index deef1cd1d7..21ee107b37 100644
--- a/library/init/meta/converter/interactive.lean
+++ b/library/init/meta/converter/interactive.lean
@@ -125,25 +125,32 @@ section rw
 open tactic.interactive (rw_rules rw_rule get_rule_eqn_lemmas to_expr')
 open tactic (rewrite_cfg)
 
-private meta def rw_lhs (h : expr) (cfg : rewrite_cfg) : conv unit :=
-do l ← conv.lhs,
-   (new_lhs, prf, _) ← tactic.rewrite h l cfg,
-   update_lhs new_lhs prf
-
-private meta def rw_core (rs : list rw_rule) (cfg : rewrite_cfg) : conv unit :=
+-- since we're in conv mode, we need to discharge all new goals immediately
+private meta def rw_lhs (h : expr) (cfg : rewrite_cfg) (tac : tactic unit) : conv unit :=
+tactic.solve1
+  (do l ← conv.lhs,
+      (new_lhs, prf, _) ← tactic.rewrite h l cfg,
+      update_lhs new_lhs prf,
+      gs' ← tactic.get_goals,
+      match gs' with
+      | [] := skip
+      | g::gs := tac
+      end)
+
+private meta def rw_core (rs : list rw_rule) (cfg : rewrite_cfg) (tac : tactic unit) : conv unit :=
 rs.mmap' $ λ r, do
  save_info r.pos,
  eq_lemmas ← get_rule_eqn_lemmas r,
  orelse'
-   (do h ← to_expr' r.rule, rw_lhs h {symm := r.symm, ..cfg})
-   (eq_lemmas.mfirst $ λ n, do e ← tactic.mk_const n, rw_lhs e {symm := r.symm, ..cfg})
+   (do h ← to_expr' r.rule, rw_lhs h {symm := r.symm, ..cfg} tac)
+   (eq_lemmas.mfirst $ λ n, do e ← tactic.mk_const n, rw_lhs e {symm := r.symm, ..cfg} tac)
    (eq_lemmas.empty)
 
 meta def rewrite (q : parse rw_rules) (cfg : rewrite_cfg := {}) : conv unit :=
-rw_core q.rules cfg
+rw_core q.rules cfg skip
 
 meta def rw (q : parse rw_rules) (cfg : rewrite_cfg := {}) : conv unit :=
-rw_core q.rules cfg
+rw_core q.rules cfg skip
 end rw
 
 end interactive