Merge PR #920: kernel: bugfix in filter_stack_domain.

2 files changed, 19 insertions, 0 deletions

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 -> 
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