diff options
| author | Pierre-Marie Pédrot | 2020-03-05 15:14:47 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-03-08 15:31:27 +0100 |
| commit | 4481b95f6f89acd7013b16a345d379dc44d67705 (patch) | |
| tree | cd1d0f1c59a3a27aa1fd777797834fc15ac71a38 /kernel/indTyping.ml | |
| parent | 6143ac9f9307b2f6863cca019a66cdcbfd52d7ce (diff) | |
Template polymorphism is now a property of the inductive block.
For an inductive block to be template, all its components must also
be. This is probably fixing a few soundness bugs in the process, but I
do not want to think too much about it.
Diffstat (limited to 'kernel/indTyping.ml')
| -rw-r--r-- | kernel/indTyping.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml index d48422909f..1d72d1bd6e 100644 --- a/kernel/indTyping.ml +++ b/kernel/indTyping.ml @@ -101,10 +101,10 @@ let check_indices_matter env_params info indices = else check_context_univs ~ctor:false env_params info indices (* env_ar contains the inductives before the current ones in the block, and no parameters *) -let check_arity env_params env_ar ind = +let check_arity ~template env_params env_ar ind = let {utj_val=arity;utj_type=_} = Typeops.infer_type env_params ind.mind_entry_arity in let indices, ind_sort = Reduction.dest_arity env_params arity in - let ind_min_univ = if ind.mind_entry_template then Some Universe.type0m else None in + let ind_min_univ = if template then Some Universe.type0m else None in let univ_info = { ind_squashed=false; ind_has_relevant_arg=false; @@ -283,7 +283,7 @@ let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) = mind_check_names mie; assert (List.is_empty (Environ.rel_context env)); - let has_template_poly = List.exists (fun oie -> oie.mind_entry_template) mie.mind_entry_inds in + let has_template_poly = mie.mind_entry_template in (* universes *) let env_univs = @@ -304,7 +304,7 @@ let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) = let env_params, params = Typeops.check_context env_univs mie.mind_entry_params in (* Arities *) - let env_ar, data = List.fold_left_map (check_arity env_params) env_univs mie.mind_entry_inds in + let env_ar, data = List.fold_left_map (check_arity ~template:has_template_poly env_params) env_univs mie.mind_entry_inds in let env_ar_par = push_rel_context params env_ar in (* Constructors *) |