From e0bcbccf437ebee4157fdfdd5cba7b42019ead27 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 6 Mar 2020 10:57:19 +0100
Subject: Ensure that template parameters are shared in the same inductive
 block.

This could have been at the root of strange behaviours (read unsoundness).
---
 kernel/declarations.ml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'kernel/declarations.ml')

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;
-- 
cgit v1.2.3