From 776bff1948b2452b315a48ca7d9ec8a6826981b3 Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Tue, 25 Jul 2023 14:16:55 -0400
Subject: [PATCH] fix: `repeat` conv should not auto-close the goal

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

diff --git a/src/Init/Conv.lean b/src/Init/Conv.lean
index 149c4e7c7a..f974028bc0 100644
--- a/src/Init/Conv.lean
+++ b/src/Init/Conv.lean
@@ -286,7 +286,7 @@ macro:1 x:conv tk:" <;> " y:conv:0 : conv =>
 /-- `repeat convs` runs the sequence `convs` repeatedly until it fails to apply. -/
 syntax "repeat " convSeq : conv
 macro_rules
-  | `(conv| repeat $seq) => `(conv| first | ($seq); repeat $seq | rfl)
+  | `(conv| repeat $seq) => `(conv| first | ($seq); repeat $seq | skip)
 
 /--
 `conv => ...` allows the user to perform targeted rewriting on a goal or hypothesis,