From fe22d84143c7ea93ad33cac3d93b083f750883f7 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 15 Jun 2022 15:48:11 +0200
Subject: [PATCH] fix: unclear TSyntax breakage

---
 src/Init/Tactics.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
index b959d68fcf..fd7c8a631e 100644
--- a/src/Init/Tactics.lean
+++ b/src/Init/Tactics.lean
@@ -285,7 +285,7 @@ macro "have " d:haveDecl : tactic => `(refine_lift have $d:haveDecl; ?_)
 /--
 `have h := e` adds the hypothesis `h : t` if `e : t`.
 -/
-macro (priority := high) "have" x:ident " := " p:term : tactic => `(have $x:ident : _ := $p)
+macro  (name := «tacticHave__:=_») (priority := high) "have" x:ident " := " p:term : tactic => `(have $x:ident : _ := $p)
 /--
 Given a main goal `ctx |- t`, `suffices h : t' from e` replaces the main goal with `ctx |- t'`,
 `e` must have type `t` in the context `ctx, h : t'`.