fix: unclear TSyntax breakage

leanprover · Jun 24, 2022 · e71e4ac · e71e4ac
1 parent 4efeef2
commit e71e4ac
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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'`.