diff options
| author | Matthieu Sozeau | 2014-11-22 19:34:25 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-11-23 15:28:41 +0100 |
| commit | ff0a051caf031fb427007714f6325c74b8893702 (patch) | |
| tree | fbb4b2fae772c9a0fe6a8b5d7310eb60dae7c045 /kernel | |
| parent | c81065e5cdc6d803bd67eccf93dc8fbb640c6892 (diff) | |
Pass around information on the use of template polymorphism for
inductive types (i.e., ones declared with an explicit anonymous Type
at the conclusion of their arity). With this change one can force
inductives to live in higher universes even in the non-fully universe
polymorphic case (e.g. bug #3821).
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/entries.mli | 3 | ||||
| -rw-r--r-- | kernel/indtypes.ml | 9 |
2 files changed, 7 insertions, 5 deletions
diff --git a/kernel/entries.mli b/kernel/entries.mli index f6958849b0..baeec31b4b 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -37,6 +37,7 @@ then, in i{^ th} block, [mind_entry_params] is [xn:Xn;...;x1:X1]; type one_inductive_entry = { mind_entry_typename : Id.t; mind_entry_arity : constr; + mind_entry_template : bool; (* Use template polymorphism *) mind_entry_consnames : Id.t list; mind_entry_lc : constr list } @@ -48,7 +49,7 @@ type mutual_inductive_entry = { mind_entry_finite : Decl_kinds.recursivity_kind; mind_entry_params : (Id.t * local_entry) list; mind_entry_inds : one_inductive_entry list; - mind_entry_polymorphic : bool; + mind_entry_polymorphic : bool; mind_entry_universes : Univ.universe_context; mind_entry_private : bool option } diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index afd7cde979..6dd3ab2ba9 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -226,7 +226,8 @@ let typecheck_inductive env ctx mie = List.fold_left (fun (env_ar,l) ind -> (* Arities (without params) are typed-checked here *) - let arity, expltype = + let expltype = ind.mind_entry_template in + let arity = if isArity ind.mind_entry_arity then let (ctx,s) = dest_arity env_params ind.mind_entry_arity in match s with @@ -237,12 +238,12 @@ let typecheck_inductive env ctx mie = let proparity = infer_type env_params (mkArity (ctx, prop_sort)) in let (cctx, _) = destArity proparity.utj_val in (* Any universe is well-formed, we don't need to check [s] here *) - mkArity (cctx, s), not (Sorts.is_small s) + mkArity (cctx, s) | _ -> let arity = infer_type env_params ind.mind_entry_arity in - arity.utj_val, not (Sorts.is_small s) + arity.utj_val else let arity = infer_type env_params ind.mind_entry_arity in - arity.utj_val, false + arity.utj_val in let (sign, deflev) = dest_arity env_params arity in let inflev = |