diff options
Diffstat (limited to 'checker/indtypes.ml')
| -rw-r--r-- | checker/indtypes.ml | 19 |
1 files changed, 9 insertions, 10 deletions
diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 277fed30..1e773df6 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: indtypes.ml 10296 2007-11-07 11:02:42Z barras $ *) - open Util open Names open Univ @@ -178,7 +176,7 @@ let check_predicativity env s small level = Type u, _ -> let u' = fresh_local_univ () in let cst = - merge_constraints (enforce_geq u' u Constraint.empty) + merge_constraints (enforce_geq u' u empty_constraint) (universes env) in if not (check_geq cst u' level) then failwith "impredicative Type inductive type" @@ -394,7 +392,7 @@ let rec ienv_decompose_prod (env,_,_,_ as ienv) n c = (* The recursive function that checks positivity and builds the list of recursive arguments *) -let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp i indlc = +let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp (_,i as ind) indlc = let lparams = rel_context_length hyps in (* check the inductive types occur positively in [c] *) let rec check_pos (env, n, ntypes, ra_env as ienv) c = @@ -496,7 +494,7 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp i indlc = with IllFormedInd err -> explain_ind_err (ntypes-i) env lparams c err) indlc - in mk_paths (Mrec i) irecargs + in mk_paths (Mrec ind) irecargs let check_subtree (t1:'a) (t2:'a) = if not (Rtree.compare_rtree (fun t1 t2 -> @@ -507,16 +505,17 @@ let check_subtree (t1:'a) (t2:'a) = failwith "bad recursive trees" (* if t1=t2 then () else msg_warning (str"TODO: check recursive positions")*) -let check_positivity env_ar params nrecp inds = +let check_positivity env_ar mind params nrecp inds = let ntypes = Array.length inds in - let rc = Array.mapi (fun j t -> (Mrec j,t)) (Rtree.mk_rec_calls ntypes) in + let rc = + Array.mapi (fun j t -> (Mrec(mind,j),t)) (Rtree.mk_rec_calls ntypes) in let lra_ind = List.rev (Array.to_list rc) in let lparams = rel_context_length params in let check_one i mip = let ra_env = list_tabulate (fun _ -> (Norec,mk_norec)) lparams @ lra_ind in let ienv = (env_ar, 1+lparams, ntypes, ra_env) in - check_positivity_one ienv params nrecp i mip.mind_nf_lc + check_positivity_one ienv params nrecp (mind,i) mip.mind_nf_lc in let irecargs = Array.mapi check_one inds in let wfp = Rtree.mk_rec irecargs in @@ -549,7 +548,7 @@ let check_inductive env kn mib = (* - check constructor types *) Array.iter (typecheck_one_inductive env_ar params mib) mib.mind_packets; (* check mind_nparams_rec: positivity condition *) - check_positivity env_ar params mib.mind_nparams_rec mib.mind_packets; + check_positivity env_ar kn params mib.mind_nparams_rec mib.mind_packets; (* check mind_equiv... *) (* Now we can add the inductive *) add_mind kn mib env |