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).
---
 checker/values.ml | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

(limited to 'checker/values.ml')

diff --git a/checker/values.ml b/checker/values.ml
index ed730cff8e..cba96e6636 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -227,8 +227,11 @@ let v_oracle =
     v_pred v_cst;
   |]
 
-let v_pol_arity =
-  v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ;v_context_set|]
+let v_template_arity =
+  v_tuple "template_arity" [|v_univ|]
+
+let v_template_universes =
+  v_tuple "template_universes" [|List(Opt v_level);v_context_set|]
 
 let v_primitive =
   v_enum "primitive" 44 (* Number of "Primitive" in Int63.v and PrimFloat.v *)
@@ -265,7 +268,7 @@ let v_mono_ind_arity =
   v_tuple "monomorphic_inductive_arity" [|v_constr;v_sort|]
 
 let v_ind_arity = v_sum "inductive_arity" 0
-  [|[|v_mono_ind_arity|];[|v_pol_arity|]|]
+  [|[|v_mono_ind_arity|];[|v_template_arity|]|]
 
 let v_one_ind = v_tuple "one_inductive_body"
   [|v_id;
@@ -301,6 +304,7 @@ let v_ind_pack = v_tuple "mutual_inductive_body"
     Int;
     v_rctxt;
     v_univs; (* universes *)
+    Opt v_template_universes;
     Opt (Array v_variance);
     Opt (Array v_variance);
     Opt v_bool;
-- 
cgit v1.2.3