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.

1 files changed, 10 insertions, 4 deletions

diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml
index 62e732ce69..b93b03ec16 100644
--- a/checker/checkInductive.ml
+++ b/checker/checkInductive.ml
@@ -52,20 +52,19 @@ let to_entry mind (mb:mutual_inductive_body) : Entries.mutual_inductive_entry =
     | Polymorphic auctx -> Polymorphic_entry (AUContext.names auctx, AUContext.repr auctx)
   in
   let mind_entry_inds = Array.map_to_list (fun ind ->
-      let mind_entry_arity, mind_entry_template = match ind.mind_arity with
+      let mind_entry_arity = match ind.mind_arity with
         | RegularArity ar ->
           let ctx, arity = Term.decompose_prod_n_assum nparams ar.mind_user_arity in
           ignore ctx; (* we will check that the produced user_arity is equal to the input *)
-          arity, false
+          arity
         | TemplateArity ar ->
           let ctx = ind.mind_arity_ctxt in
           let ctx = List.firstn (List.length ctx - nparams) ctx in
-          Term.mkArity (ctx, Sorts.sort_of_univ ar.template_level), true
+          Term.mkArity (ctx, Sorts.sort_of_univ ar.template_level)
       in
       {
         mind_entry_typename = ind.mind_typename;
         mind_entry_arity;
-        mind_entry_template;
         mind_entry_consnames = Array.to_list ind.mind_consnames;
         mind_entry_lc = Array.map_to_list (fun c ->
             let ctx, c = Term.decompose_prod_n_assum nparams c in
@@ -75,12 +74,19 @@ let to_entry mind (mb:mutual_inductive_body) : Entries.mutual_inductive_entry =
       })
       mb.mind_packets
   in
+  let check_template ind = match ind.mind_arity with
+  | RegularArity _ -> false
+  | TemplateArity _ -> true
+  in
+  let mind_entry_template = Array.exists check_template mb.mind_packets in
+  let () = if mind_entry_template then assert (Array.for_all check_template mb.mind_packets) in
   {
     mind_entry_record;
     mind_entry_finite = mb.mind_finite;
     mind_entry_params = mb.mind_params_ctxt;
     mind_entry_inds;
     mind_entry_universes;
+    mind_entry_template;
     mind_entry_cumulative= Option.has_some mb.mind_variance;
     mind_entry_private = mb.mind_private;
   }