Merge branch 'v8.5'

1 files changed, 12 insertions, 7 deletions

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 4834f95d1..33abfe5b7 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -465,7 +465,7 @@ let array_min nmr a = if Int.equal nmr 0 then 0 else
     considered sub-terms) as well as the number of of non-uniform
     arguments (used to generate induction schemes, so a priori less
     relevant to the kernel). *)
-let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcnames indlc =
+let check_positivity_one recursive (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcnames indlc =
   let lparams = Context.Rel.length hyps in
   let nmr = Context.Rel.nhyps hyps in
   (** Positivity of one argument [c] of a constructor (i.e. the
@@ -580,6 +580,8 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname
 
           | Prod (na,b,d) ->
 	      let () = assert (List.is_empty largs) in
+	      if not recursive && not (noccur_between n ntypes b) then
+	        raise (InductiveError BadEntry);
               let nmr',recarg = check_pos ienv nmr b in
               let ienv' = ienv_push_var ienv (na,b,mk_norec) in
                 check_constr_rec ienv' nmr' (recarg::lrec) d
@@ -614,9 +616,11 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname
 
 (** [check_positivity kn env_ar params] checks that the mutually
     inductive block [inds] is strictly positive. *)
-let check_positivity kn env_ar params inds =
+let check_positivity kn env_ar params finite inds =
   let ntypes = Array.length inds in
-  let rc = Array.mapi (fun j t -> (Mrec (kn,j),t)) (Rtree.mk_rec_calls ntypes) in
+  let recursive = finite != Decl_kinds.BiFinite in
+  let rc = Array.mapi (fun j t -> (Mrec (kn,j),t))
+		      (Rtree.mk_rec_calls ntypes) in
   let lra_ind = Array.rev_to_list rc in
   let lparams = Context.Rel.length params in
   let nmr = Context.Rel.nhyps params in
@@ -625,7 +629,7 @@ let check_positivity kn env_ar params inds =
       List.init lparams (fun _ -> (Norec,mk_norec)) @ lra_ind in
     let ienv = (env_ar, 1+lparams, ntypes, ra_env) in
     let nargs = Context.Rel.nhyps sign - nmr in
-    check_positivity_one ienv params (kn,i) nargs lcnames lc
+    check_positivity_one recursive ienv params (kn,i) nargs lcnames lc
   in
   let irecargs_nmr = Array.mapi check_one inds in
   let irecargs = Array.map snd irecargs_nmr
@@ -850,10 +854,11 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re
 	mind_reloc_tbl = rtbl;
       } in
   let packets = Array.map2 build_one_packet inds recargs in
-  let pkt = packets.(0) in	  
+  let pkt = packets.(0) in
   let isrecord = 
     match isrecord with
-    | Some (Some rid) when pkt.mind_kelim == all_sorts && Array.length pkt.mind_consnames == 1
+    | Some (Some rid) when pkt.mind_kelim == all_sorts
+			   && Array.length pkt.mind_consnames == 1
 			   && pkt.mind_consnrealargs.(0) > 0 ->
       (** The elimination criterion ensures that all projections can be defined. *)
       let u = 
@@ -894,7 +899,7 @@ let check_inductive env kn mie =
   (* First type-check the inductive definition *)
   let (env_ar, env_ar_par, params, inds) = typecheck_inductive env mie in
   (* Then check positivity conditions *)
-  let (nmr,recargs) = check_positivity kn env_ar_par params inds in
+  let (nmr,recargs) = check_positivity kn env_ar_par params mie.mind_entry_finite inds in
   (* Build the inductive packets *)
     build_inductive env mie.mind_entry_polymorphic mie.mind_entry_private
       mie.mind_entry_universes