From ab8627d929d4342b984e4eacc40fbad39eb91e0c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 1 Sep 2021 19:27:13 -0700
Subject: [PATCH] chore: update stage0

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

diff --git a/stage0/src/Init/Conv.lean b/stage0/src/Init/Conv.lean
index 819224cd8e..e4935cee5f 100644
--- a/stage0/src/Init/Conv.lean
+++ b/stage0/src/Init/Conv.lean
@@ -25,7 +25,7 @@ syntax (name := nestedConv) convSeqBracketed : conv
 syntax (name := paren) "(" convSeq ")" : conv
 
 /-- `· conv` focuses on the main conv goal and tries to solve it using `s` -/
-macro dot:("·" <|> ".") s:convSeq : conv => `(conv| {%$dot ($s:convSeq) })
+macro dot:("·" <|> ".") s:convSeq : conv => `({%$dot ($s:convSeq) })
 
 syntax (name := conv) "conv " (" at " ident)? (" in " term)? " => " convSeq : tactic