kernel: bugfix in filter_stack_domain.

It did not consider that the argument might be higher-order, e.g. [nat -> I].

1 files changed, 2 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 ->