From 71229f45fbc3f5063bcd2f8f314320555c784630 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 12 Sep 2021 18:30:08 -0700 Subject: [PATCH] chore: "upgrate" to doc string --- src/Init/Notation.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean index bdda844f90..af69e0dcf7 100644 --- a/src/Init/Notation.lean +++ b/src/Init/Notation.lean @@ -320,7 +320,7 @@ macro "admit" : tactic => `(exact sorry) macro "sorry" : tactic => `(exact sorry) macro "inferInstance" : tactic => `(exact inferInstance) -/- Optional configuration option for tactics -/ +/-- Optional configuration option for tactics -/ syntax config := ("(" &"config" " := " term ")") syntax locationWildcard := "*"