From 6143ac9f9307b2f6863cca019a66cdcbfd52d7ce Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 7 Feb 2020 17:10:49 +0100
Subject: Do not hardcode specific handling of Prop levels in template poly.

We also factorize a few checks by returning an option when looking for
a potentially template universe.
---
 vernac/comInductive.ml | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

(limited to 'vernac/comInductive.ml')

diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index edb03a5c89..08a8d1b320 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -329,10 +329,7 @@ let template_polymorphism_candidate ~ctor_levels uctx params concl =
     if not concltemplate then false
     else
       let conclu = Option.cata Sorts.univ_of_sort Univ.type0m_univ concl in
-      let params, conclunivs =
-        IndTyping.template_polymorphic_univs ~ctor_levels uctx params conclu
-      in
-      not (Univ.LSet.is_empty conclunivs)
+      Option.has_some @@ IndTyping.template_polymorphic_univs ~ctor_levels uctx params conclu
   | Entries.Polymorphic_entry _ -> false
 
 let check_param = function
-- 
cgit v1.2.3


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.
---
 vernac/comInductive.ml | 20 ++++++++++++--------
 1 file changed, 12 insertions(+), 8 deletions(-)

(limited to 'vernac/comInductive.ml')

diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 08a8d1b320..718e62b9b7 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -367,6 +367,14 @@ let interp_mutual_inductive_constr ~sigma ~template ~udecl ~ctx_params ~indnames
 
   (* Build the inductive entries *)
   let entries = List.map4 (fun indname (templatearity, arity) concl (cnames,ctypes) ->
+      { mind_entry_typename = indname;
+        mind_entry_arity = arity;
+        mind_entry_consnames = cnames;
+        mind_entry_lc = ctypes
+      })
+      indnames arities arityconcl constructors
+  in
+  let template = List.map4 (fun indname (templatearity, _) concl (_, ctypes) ->
       let template_candidate () =
         templatearity ||
         let ctor_levels =
@@ -382,22 +390,17 @@ let interp_mutual_inductive_constr ~sigma ~template ~udecl ~ctx_params ~indnames
         in
         template_polymorphism_candidate ~ctor_levels uctx ctx_params concl
       in
-      let template = match template with
+      match template with
         | Some template ->
           if poly && template then user_err
               Pp.(strbrk "Template-polymorphism and universe polymorphism are not compatible.");
           template
         | None ->
           should_auto_template indname (template_candidate ())
-      in
-      { mind_entry_typename = indname;
-        mind_entry_arity = arity;
-        mind_entry_template = template;
-        mind_entry_consnames = cnames;
-        mind_entry_lc = ctypes
-      })
+      )
       indnames arities arityconcl constructors
   in
+  let is_template = List.for_all (fun t -> t) template in
   (* Build the mutual inductive entry *)
   let mind_ent =
     { mind_entry_params = ctx_params;
@@ -406,6 +409,7 @@ let interp_mutual_inductive_constr ~sigma ~template ~udecl ~ctx_params ~indnames
       mind_entry_inds = entries;
       mind_entry_private = if private_ind then Some false else None;
       mind_entry_universes = uctx;
+      mind_entry_template = is_template;
       mind_entry_cumulative = poly && cumulative;
     }
   in
-- 
cgit v1.2.3