From 42c3741667aebda318d5f50ce7a4c105a32703a7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9o=20Winterhalter?= <theo.winterhalter@gmail.com>
Date: Tue, 30 Jul 2024 10:18:31 +0200
Subject: [PATCH] rasimpl: add one repeat

---
 theories/SubstNotations.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/SubstNotations.v b/theories/SubstNotations.v
index 9a0e700..b37d5e3 100644
--- a/theories/SubstNotations.v
+++ b/theories/SubstNotations.v
@@ -735,7 +735,7 @@ Ltac setoid_rasimpl1_t t :=
 Ltac rasimpl1_aux tac g :=
   let rec aux t :=
     first [
-      progress (tac t)
+      progress (repeat (tac t))
     | lazymatch t with
       | subst_cterm ?s _ => aux s
       | ren_cterm ?r _ => aux r