From 8ffa07ab254a5bd426944dff072e7b8b7871d24b Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 7 Jun 2022 17:43:16 +0200
Subject: [PATCH] fix: goal state on `conv =>`

---
 src/Init/Conv.lean                                 |  4 +++-
 src/Lean/Elab/Tactic/Conv/Basic.lean               |  2 +-
 tests/lean/interactive/plainGoal.lean              |  7 ++++++-
 tests/lean/interactive/plainGoal.lean.expected.out | 10 ++++++++--
 4 files changed, 18 insertions(+), 5 deletions(-)

diff --git a/src/Init/Conv.lean b/src/Init/Conv.lean
index 38f59a6c08..b206572b4a 100644
--- a/src/Init/Conv.lean
+++ b/src/Init/Conv.lean
@@ -14,7 +14,9 @@ declare_syntax_cat conv (behavior := both)
 
 syntax convSeq1Indented := withPosition((group(colGe conv ";"?))+)
 syntax convSeqBracketed := "{" (group(conv ";"?))+ "}"
-syntax convSeq := convSeq1Indented <|> convSeqBracketed
+-- Order is important: a missing `conv` proof should not be parsed as `{ <missing> }`,
+-- automatically closing goals
+syntax convSeq := convSeqBracketed <|> convSeq1Indented
 
 syntax (name := conv) "conv " (" at " ident)? (" in " term)? " => " convSeq : tactic
 
diff --git a/src/Lean/Elab/Tactic/Conv/Basic.lean b/src/Lean/Elab/Tactic/Conv/Basic.lean
index c4773b7c85..2e8360c972 100644
--- a/src/Lean/Elab/Tactic/Conv/Basic.lean
+++ b/src/Lean/Elab/Tactic/Conv/Basic.lean
@@ -131,7 +131,7 @@ def remarkAsConvGoal : TacticM Unit := do
 
 private def convTarget (conv : Syntax) : TacticM Unit := withMainContext do
    let target ← getMainTarget
-   let (targetNew, proof) ← convert target (evalTactic conv)
+   let (targetNew, proof) ← convert target (withTacticInfoContext (← getRef) (evalTactic conv))
    liftMetaTactic1 fun mvarId => replaceTargetEq mvarId targetNew proof
    evalTactic (← `(tactic| try rfl))
 
diff --git a/tests/lean/interactive/plainGoal.lean b/tests/lean/interactive/plainGoal.lean
index b7598f34bf..556fe1578e 100644
--- a/tests/lean/interactive/plainGoal.lean
+++ b/tests/lean/interactive/plainGoal.lean
@@ -88,11 +88,16 @@ example : True := (by exact True.intro)
 example : True := (by exact True.intro )
                                      --^ $/lean/plainGoal
 
-set_option trace.Elab.info true
 example : True ∧ False := by
   · constructor; constructor
               --^ $/lean/plainGoal
 
+example : True = True := by
+  conv =>
+      --^ $/lean/plainGoal
+    --
+  --^ $/lean/plainGoal
+
 example : False := by
 -- EOF test
 --^ $/lean/plainGoal
diff --git a/tests/lean/interactive/plainGoal.lean.expected.out b/tests/lean/interactive/plainGoal.lean.expected.out
index a48b773e0f..75235ff021 100644
--- a/tests/lean/interactive/plainGoal.lean.expected.out
+++ b/tests/lean/interactive/plainGoal.lean.expected.out
@@ -114,10 +114,16 @@
  "position": {"line": 87, "character": 39}}
 null
 {"textDocument": {"uri": "file://plainGoal.lean"},
- "position": {"line": 92, "character": 16}}
+ "position": {"line": 91, "character": 16}}
 {"rendered":
  "```lean\ncase left\n⊢ True\n```\n---\n```lean\ncase right\n⊢ False\n```",
  "goals": ["case left\n⊢ True", "case right\n⊢ False"]}
 {"textDocument": {"uri": "file://plainGoal.lean"},
- "position": {"line": 96, "character": 2}}
+ "position": {"line": 95, "character": 8}}
+{"rendered": "```lean\n| True = True\n```", "goals": ["| True = True"]}
+{"textDocument": {"uri": "file://plainGoal.lean"},
+ "position": {"line": 97, "character": 4}}
+{"rendered": "```lean\n| True = True\n```", "goals": ["| True = True"]}
+{"textDocument": {"uri": "file://plainGoal.lean"},
+ "position": {"line": 101, "character": 2}}
 {"rendered": "```lean\n⊢ False\n```", "goals": ["⊢ False"]}