From a62d412dce82d11612469bf492f416cdc1f3fe40 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 15 Mar 2023 16:51:29 +0100
Subject: [PATCH] =?UTF-8?q?fix:=20implement=20`=C2=B7=20tacs`=20as=20a=20b?=
 =?UTF-8?q?uiltin=20elaborator,=20part=202?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Fixes #2153
---
 src/Init/NotationExtra.lean                        | 5 -----
 src/Lean/Elab/BuiltinTerm.lean                     | 2 +-
 tests/lean/interactive/plainGoal.lean              | 1 -
 tests/lean/interactive/plainGoal.lean.expected.out | 3 +--
 4 files changed, 2 insertions(+), 9 deletions(-)

diff --git a/src/Init/NotationExtra.lean b/src/Init/NotationExtra.lean
index 145c9bde3c..1b756a8505 100644
--- a/src/Init/NotationExtra.lean
+++ b/src/Init/NotationExtra.lean
@@ -372,14 +372,9 @@ macro_rules
     `($mods:declModifiers class $id $params* extends $parents,* $[: $ty]?
       attribute [instance] $ctor)
 
-section
-open Lean.Parser.Tactic
 syntax cdotTk := patternIgnore("· " <|> ". ")
 /-- `· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. -/
 syntax (name := cdot) cdotTk tacticSeqIndentGt : tactic
-macro_rules
-  | `(tactic| $cdot:cdotTk $tacs) => `(tactic| {%$cdot ($tacs) }%$cdot)
-end
 
 /--
   Similar to `first`, but succeeds only if one the given tactics solves the current goal.
diff --git a/src/Lean/Elab/BuiltinTerm.lean b/src/Lean/Elab/BuiltinTerm.lean
index cd9cebafa7..31516619b0 100644
--- a/src/Lean/Elab/BuiltinTerm.lean
+++ b/src/Lean/Elab/BuiltinTerm.lean
@@ -157,7 +157,7 @@ private def mkTacticMVar (type : Expr) (tacticCode : Syntax) : TermElabM Expr :=
 @[builtin_term_elab noImplicitLambda] def elabNoImplicitLambda : TermElab := fun stx expectedType? =>
   elabTerm stx[1] (mkNoImplicitLambdaAnnotation <$> expectedType?)
 
-@[builtin_term_elab cdot] def elabBadCDot : TermElab := fun _ _ =>
+@[builtin_term_elab Lean.Parser.Term.cdot] def elabBadCDot : TermElab := fun _ _ =>
   throwError "invalid occurrence of `·` notation, it must be surrounded by parentheses (e.g. `(· + 1)`)"
 
 @[builtin_term_elab str] def elabStrLit : TermElab := fun stx _ => do
diff --git a/tests/lean/interactive/plainGoal.lean b/tests/lean/interactive/plainGoal.lean
index 8c01cc9a0c..2b6c78aed3 100644
--- a/tests/lean/interactive/plainGoal.lean
+++ b/tests/lean/interactive/plainGoal.lean
@@ -134,4 +134,3 @@ example : True ∧ False := by
   · --
  --^ $/lean/plainGoal
   --^ $/lean/plainGoal
-  -- TODO: ^
diff --git a/tests/lean/interactive/plainGoal.lean.expected.out b/tests/lean/interactive/plainGoal.lean.expected.out
index 9daa64761d..70565ea534 100644
--- a/tests/lean/interactive/plainGoal.lean.expected.out
+++ b/tests/lean/interactive/plainGoal.lean.expected.out
@@ -169,5 +169,4 @@ null
 {"rendered": "```lean\ncase left\n⊢ True\n```", "goals": ["case left\n⊢ True"]}
 {"textDocument": {"uri": "file://plainGoal.lean"},
  "position": {"line": 133, "character": 4}}
-{"rendered": "```lean\ncase right\n⊢ False\n```",
- "goals": ["case right\n⊢ False"]}
+{"rendered": "```lean\ncase left\n⊢ True\n```", "goals": ["case left\n⊢ True"]}