diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/indtypes.ml | 7 | ||||
| -rw-r--r-- | kernel/inductive.ml | 4 | ||||
| -rw-r--r-- | kernel/inductive.mli | 3 | ||||
| -rw-r--r-- | kernel/univ.ml | 5 | ||||
| -rw-r--r-- | kernel/univ.mli | 2 |
5 files changed, 18 insertions, 3 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index cd9e2e81f4..5786e67d53 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -254,10 +254,13 @@ let typecheck_inductive env mie = array_fold_map2' (fun ((id,full_arity,ar_level),cn,info,lc,_) lev cst -> let sign, s = dest_arity env full_arity in let status,cst = match s with - | Type _ when ar_level <> None (* Explicitly polymorphic *) -> + | Type u when ar_level <> None (* Explicitly polymorphic *) + && no_upper_constraints u cst -> (* The polymorphic level is a function of the level of the *) (* conclusions of the parameters *) - Inr (param_ccls, lev), cst + (* We enforce [u >= lev] in case [lev] has a strict upper *) + (* constraints over [u] *) + Inr (param_ccls, lev), enforce_geq u lev cst | Type u (* Not an explicit occurrence of Type *) -> Inl (info,full_arity,s), enforce_geq u lev cst | Prop Pos when engagement env <> Some ImpredicativeSet -> diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 8ff8ddb85e..918a32c956 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -228,7 +228,9 @@ let arities_of_specif kn (mib,mip) = let arities_of_constructors ind specif = arities_of_specif (fst ind) specif - +let type_of_constructors ind (mib,mip) = + let specif = mip.mind_user_lc in + Array.map (constructor_instantiate (fst ind) mib) specif (************************************************************************) diff --git a/kernel/inductive.mli b/kernel/inductive.mli index e63c7772c3..118d19830e 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -47,6 +47,9 @@ val type_of_constructor : constructor -> mind_specif -> types (* Return constructor types in normal form *) val arities_of_constructors : inductive -> mind_specif -> types array +(* Return constructor types in user form *) +val type_of_constructors : inductive -> mind_specif -> types array + (* Transforms inductive specification into types (in nf) *) val arities_of_specif : mutual_inductive -> mind_specif -> types array diff --git a/kernel/univ.ml b/kernel/univ.ml index 001ee3ea8a..a681210acf 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -550,6 +550,11 @@ let subst_large_constraint u u' v = let subst_large_constraints = List.fold_right (fun (u,u') -> subst_large_constraint u u') +let no_upper_constraints u cst = + match u with + | Atom u -> Constraint.for_all (fun (u1,_,_) -> u1 <> u) cst + | Max _ -> anomaly "no_upper_constraints" + (* Pretty-printing *) let num_universes g = diff --git a/kernel/univ.mli b/kernel/univ.mli index 1ce5329ab9..225dce9a6c 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -76,6 +76,8 @@ val subst_large_constraint : universe -> universe -> universe -> universe val subst_large_constraints : (universe * universe) list -> universe -> universe +val no_upper_constraints : universe -> constraints -> bool + (*s Pretty-printing of universes. *) val pr_uni : universe -> Pp.std_ppcmds |