diff options
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 = |