From 4481b95f6f89acd7013b16a345d379dc44d67705 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 5 Mar 2020 15:14:47 +0100
Subject: 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.
---
 kernel/entries.ml   | 2 +-
 kernel/indTyping.ml | 8 ++++----
 2 files changed, 5 insertions(+), 5 deletions(-)

(limited to 'kernel')

diff --git a/kernel/entries.ml b/kernel/entries.ml
index 8d930b521c..983fa822e9 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -37,7 +37,6 @@ 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 }
 
@@ -50,6 +49,7 @@ type mutual_inductive_entry = {
   mind_entry_params : Constr.rel_context;
   mind_entry_inds : one_inductive_entry list;
   mind_entry_universes : universes_entry;
+  mind_entry_template : bool; (* Use template polymorphism *)
   mind_entry_cumulative : bool;
   (* universe constraints and the constraints for subtyping of
      inductive types in the block. *)
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 *)
-- 
cgit v1.2.3