From 8a249bddd2b70663f75ae83267e1688b428757f4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 3 Sep 2021 08:14:47 -0700
Subject: [PATCH] feat: add `try rfl` at end of `convTarget`

---
 src/Lean/Elab/Tactic/Conv/Basic.lean | 1 +
 tests/lean/conv1.lean                | 3 ---
 tests/lean/conv1.lean.expected.out   | 3 +++
 tests/lean/run/conv1.lean            | 2 --
 4 files changed, 4 insertions(+), 5 deletions(-)

diff --git a/src/Lean/Elab/Tactic/Conv/Basic.lean b/src/Lean/Elab/Tactic/Conv/Basic.lean
index 160cb0b67b..c34c782b06 100644
--- a/src/Lean/Elab/Tactic/Conv/Basic.lean
+++ b/src/Lean/Elab/Tactic/Conv/Basic.lean
@@ -111,6 +111,7 @@ private def convTarget (conv : Syntax) : TacticM Unit := withMainContext do
    let target ← getMainTarget
    let (targetNew, proof) ← convert target (evalTactic conv)
    liftMetaTactic1 fun mvarId => replaceTargetEq mvarId targetNew proof
+   evalTactic (← `(tactic| try rfl))
 
 private def convLocalDecl (conv : Syntax) (hUserName : Name) : TacticM Unit := withMainContext do
    let localDecl ← getLocalDeclFromUserName hUserName
diff --git a/tests/lean/conv1.lean b/tests/lean/conv1.lean
index d7f82da762..6b6bdd33c3 100644
--- a/tests/lean/conv1.lean
+++ b/tests/lean/conv1.lean
@@ -51,7 +51,6 @@ example (x y : Nat) : f x (x + y + 0) y = y + x := by
     change x + y
     traceState
     rw [Nat.add_comm]
-  rfl
 
 example : id (fun x y => 0 + x + y) = Nat.add := by
   conv =>
@@ -61,11 +60,9 @@ example : id (fun x y => 0 + x + y) = Nat.add := by
     traceState
     rw [Nat.zero_add]
     traceState
-  rfl
 
 example : id (fun x y => 0 + x + y) = Nat.add := by
   conv =>
     enter [1, 1, a, b]
     traceState
     rw [Nat.zero_add]
-  rfl
diff --git a/tests/lean/conv1.lean.expected.out b/tests/lean/conv1.lean.expected.out
index 31e324f14d..bb90fb3c0f 100644
--- a/tests/lean/conv1.lean.expected.out
+++ b/tests/lean/conv1.lean.expected.out
@@ -13,3 +13,6 @@ a b : Nat
 ⊢ 0 + a + b
 a b : Nat
 ⊢ a + b
+case h.h
+a b : Nat
+⊢ 0 + a + b
diff --git a/tests/lean/run/conv1.lean b/tests/lean/run/conv1.lean
index 5d8b41b6e1..d8c55d041d 100644
--- a/tests/lean/run/conv1.lean
+++ b/tests/lean/run/conv1.lean
@@ -40,7 +40,6 @@ example (x y : Nat) : p (x + y) (0 + y + x) := by
     traceState
     skip
     done
-  rfl
 
 axiom div_self (x : Nat) : x ≠ 0 → x / x = 1
 
@@ -69,4 +68,3 @@ example : id (fun x => 0 + x) = id := by
     arg 1
     funext y
     rw [Nat.zero_add]
-  rfl