From 6849cac7fe278c5b4238970160f754505f42773a Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 26 Jul 2017 17:21:34 +0200
Subject: kernel: bugfix in filter_stack_domain.

It did not consider that the argument might be higher-order, e.g. [nat -> I].
---
 kernel/inductive.ml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 1eaba49aa9..a393073689 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -860,6 +860,8 @@ let filter_stack_domain env ci p stack =
     match stack, kind_of_term t with
     | elt :: stack', Prod (n,a,c0) ->
       let d = LocalAssum (n,a) in
+      let ctx, a = dest_prod_assum env a in
+      let env = push_rel_context ctx env in
       let ty, args = decompose_app (whd_all env a) in
       let elt = match kind_of_term ty with
       | Ind ind -> 
-- 
cgit v1.2.3


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