Imported Upstream version 8.8.2upstream/8.8.2

1 files changed, 17 insertions, 0 deletions

diff --git a/test-suite/success/guard.v b/test-suite/success/guard.v
index b9181d43..3a1c6dab 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.