From d6aa9482b7f0e09e06b844c59950211ca3bf9270 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 18 Sep 2017 16:01:22 +0200
Subject: Add test-suite script by Cyprien Mangin

---
 test-suite/success/guard.v | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

diff --git a/test-suite/success/guard.v b/test-suite/success/guard.v
index b9181d430a..83d47dc683 100644
--- a/test-suite/success/guard.v
+++ b/test-suite/success/guard.v
@@ -9,3 +9,20 @@ Check let x (f:nat->nat) k := f k in
         | 0 => 0
         | S k => f F k (* here Rel 3 = F ! *)
         end.
+
+(** Commutation of guard condition allows recursive calls on functional arguments,
+    despite rewriting in their domain types.  *)
+Inductive foo : Type -> Type :=
+| End A : foo A
+| Next A : (A -> foo A) -> foo A.
+
+Definition nat : Type := nat.
+
+Fixpoint bar (A : Type) (e : nat = A) (f : foo A) {struct f} : nat :=
+match f with
+| End _ => fun _ => O
+| Next A g => fun e =>
+    match e in (_ = B) return (B -> foo A) -> nat with
+    | eq_refl => fun (g' : nat -> foo A) => bar A e (g' O)
+    end g
+end e.
\ No newline at end of file
-- 
cgit v1.2.3