1 files changed, 11 insertions, 0 deletions
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index 880b5da11f..9dd7b273d6 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -198,3 +198,14 @@ Goal forall x : nat, x = 1 -> x + x + x = 3.
 intros x H.
 test x 2.
 Abort.
+
+(* Utilisation de let rec sans arguments *)
+
+Ltac is := 
+  let rec i := match goal with |- ?A -> ?B => intro; i | _ => idtac end in
+  i.
+
+Goal True -> True -> True.
+is.
+exact I.
+Abort.