Ensure that template parameters are shared in the same inductive block.

This could have been at the root of strange behaviours (read unsoundness).

1 files changed, 6 insertions, 1 deletions

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index ac130d018d..11a07ee5cf 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -30,8 +30,11 @@ type engagement = set_predicativity
 *)
 
 type template_arity = {
-  template_param_levels : Univ.Level.t option list;
   template_level : Univ.Universe.t;
+}
+
+type template_universes = {
+  template_param_levels : Univ.Level.t option list;
   template_context : Univ.ContextSet.t;
 }
 
@@ -218,6 +221,8 @@ type mutual_inductive_body = {
 
     mind_universes : universes; (** Information about monomorphic/polymorphic/cumulative inductives and their universes *)
 
+    mind_template : template_universes option;
+
     mind_variance : Univ.Variance.t array option; (** Variance info, [None] when non-cumulative. *)
 
     mind_sec_variance : Univ.Variance.t array option;