From 5febd46805ea65cbcbb7c0690e20144bb4a1c234 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Fri, 5 Oct 2018 12:37:57 +0000
Subject: [coqchk] Fix guard condition with commutative cuts

---
 checker/inductive.ml | 2 ++
 1 file changed, 2 insertions(+)

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 -> 
-- 
cgit v1.2.3