Store the template polymorphic context inside the TemplateArity node.

This was the only part in the kernel that really relied on the contents
of the Monomorphic node.

6 files changed, 9 insertions, 6 deletions

diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml
index a2cf44389e..66d7e9cfee 100644
--- a/checker/checkInductive.ml
+++ b/checker/checkInductive.ml
@@ -69,8 +69,9 @@ let check_arity env ar1 ar2 = match ar1, ar2 with
   | RegularArity ar, RegularArity {mind_user_arity;mind_sort} ->
     Constr.equal ar.mind_user_arity mind_user_arity &&
     Sorts.equal ar.mind_sort mind_sort
-  | TemplateArity ar, TemplateArity {template_param_levels;template_level} ->
+  | TemplateArity ar, TemplateArity {template_param_levels;template_level;template_context} ->
     List.equal (Option.equal Univ.Level.equal) ar.template_param_levels template_param_levels &&
+    ContextSet.equal template_context ar.template_context &&
     UGraph.check_leq (universes env) template_level ar.template_level
     (* template_level is inferred by indtypes, so functor application can produce a smaller one *)
   | (RegularArity _ | TemplateArity _), _ -> assert false
diff --git a/checker/values.ml b/checker/values.ml
index fff166f27b..c8bbc092b4 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -228,7 +228,7 @@ let v_oracle =
   |]
 
 let v_pol_arity =
-  v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ|]
+  v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ;v_context_set|]
 
 let v_primitive =
   v_enum "primitive" 44 (* Number of "Primitive" in Int63.v and PrimFloat.v *)
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index cebbfe4986..f1eb000c88 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -312,14 +312,14 @@ let cook_one_ind ~template_check ~ntypes
       let arity = abstract_as_type (expmod arity) hyps in
       let sort = destSort (expmod (mkSort sort)) in
       RegularArity {mind_user_arity=arity; mind_sort=sort}
-    | TemplateArity {template_param_levels=levels;template_level} ->
+    | TemplateArity {template_param_levels=levels;template_level;template_context} ->
       let sec_levels = CList.map_filter (fun d ->
           if RelDecl.is_local_assum d then Some (template_level_of_var ~template_check d)
           else None)
           section_decls
       in
       let levels = List.rev_append sec_levels levels in
-      TemplateArity {template_param_levels=levels;template_level}
+      TemplateArity {template_param_levels=levels;template_level;template_context}
   in
   let mind_arity_ctxt =
     let ctx = Context.Rel.map expmod mip.mind_arity_ctxt in
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 0b6e59bd5e..c550b0d432 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -32,6 +32,7 @@ type engagement = set_predicativity
 type template_arity = {
   template_param_levels : Univ.Level.t option list;
   template_level : Univ.Universe.t;
+  template_context : Univ.ContextSet.t;
 }
 
 type ('a, 'b) declaration_arity =
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 27e3f84464..047027984d 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -49,7 +49,8 @@ let map_decl_arity f g = function
 let hcons_template_arity ar =
   { template_param_levels = ar.template_param_levels;
       (* List.Smart.map (Option.Smart.map Univ.hcons_univ_level) ar.template_param_levels; *)
-    template_level = Univ.hcons_univ ar.template_level }
+    template_level = Univ.hcons_univ ar.template_level;
+    template_context = Univ.hcons_universe_context_set ar.template_context }
 
 let universes_context = function
   | Monomorphic _ -> Univ.AUContext.empty
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index 591cd050a5..d5d5ec61bf 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -270,7 +270,7 @@ let abstract_packets ~template_check univs usubst params ((arity,lc),(indices,sp
         CErrors.user_err
           Pp.(strbrk "Ill-formed template inductive declaration: not polymorphic on any universe.")
       else
-        TemplateArity {template_param_levels = param_levels; template_level = min_univ}
+        TemplateArity {template_param_levels = param_levels; template_level = min_univ; template_context = ctx }
   in
 
   let kelim = allowed_sorts univ_info in