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