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(+)

(limited to 'checker/inductive.ml')

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


From 94947127d17b33de3109db3b1f3d7944493bd6c3 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Fri, 5 Oct 2018 12:50:12 +0000
Subject: [coqchk] Fix subterm relation for primitive projections

---
 checker/inductive.ml | 21 +++++++++++++++++----
 1 file changed, 17 insertions(+), 4 deletions(-)

(limited to 'checker/inductive.ml')

diff --git a/checker/inductive.ml b/checker/inductive.ml
index 44950e7ac8..89a5a5196a 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -801,10 +801,23 @@ let rec subterm_specif renv stack t =
 	    subterm_specif (push_var renv (x,a,spec)) stack' b
 
       (* Metas and evars are considered OK *)
-      | (Meta _|Evar _) -> Dead_code
-
-      (* Other terms are not subterms *)
-      | _ -> Not_subterm
+    | (Meta _|Evar _) -> Dead_code
+
+    | Proj (p, c) ->
+      let subt = subterm_specif renv stack c in
+      (match subt with
+       | Subterm (_s, wf) ->
+         (* We take the subterm specs of the constructor of the record *)
+         let wf_args = (dest_subterms wf).(0) in
+         (* We extract the tree of the projected argument *)
+         let n = Projection.arg p in
+         spec_of_tree (List.nth wf_args n)
+       | Dead_code -> Dead_code
+       | Not_subterm -> Not_subterm)
+
+    (* Other terms are not subterms *)
+    | Var _ | Sort _ | Cast _ | Prod _ | LetIn _ | App _ | Const _ | Ind _
+      | Construct _ | CoFix _ -> Not_subterm
 
 and lazy_subterm_specif renv stack t =
   lazy (subterm_specif renv stack t)
-- 
cgit v1.2.3


From dae36dcaaaf78e9b09eb644441869008144b451d Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Fri, 5 Oct 2018 12:56:28 +0000
Subject: [coqchk] Fix case_info for primitive records

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

(limited to 'checker/inductive.ml')

diff --git a/checker/inductive.ml b/checker/inductive.ml
index 89a5a5196a..5e34f04f51 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -282,6 +282,11 @@ let get_instantiated_arity (ind,u) (mib,mip) params =
 
 let elim_sorts (_,mip) = mip.mind_kelim
 
+let is_primitive_record (mib,_) =
+  match mib.mind_record with
+  | PrimRecord _ -> true
+  | NotRecord | FakeRecord -> false
+
 let extended_rel_list n hyps =
   let rec reln l p = function
     | LocalAssum _ :: hyps -> reln (Rel (n+p) :: l) (p+1) hyps
@@ -381,12 +386,13 @@ let type_case_branches env (pind,largs) (p,pj) c =
 (* Checking the case annotation is relevant *)
 
 let check_case_info env indsp ci =
-  let (mib,mip) = lookup_mind_specif env indsp in
+  let mib, mip as spec = lookup_mind_specif env indsp in
   if
     not (eq_ind_chk indsp ci.ci_ind) ||
     (mib.mind_nparams <> ci.ci_npar) ||
     (mip.mind_consnrealdecls <> ci.ci_cstr_ndecls) ||
-    (mip.mind_consnrealargs <> ci.ci_cstr_nargs)
+    (mip.mind_consnrealargs <> ci.ci_cstr_nargs) ||
+    is_primitive_record spec
   then raise (TypeError(env,WrongCaseInfo(indsp,ci)))
 
 (************************************************************************)
-- 
cgit v1.2.3