[coqchk] Fix guard condition with commutative cuts

1 files changed, 2 insertions, 0 deletions

diff --git a/checker/inductive.ml b/checker/inductive.ml
index d15380643f..44950e7ac8 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -856,6 +856,8 @@ let filter_stack_domain env p stack =
     match stack, 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 ty with
       | Ind ind ->