From 5f508021585c3b385e603524b49a25ecc65cfa7d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 5 Feb 2020 15:39:17 +0100
Subject: 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.
---
 kernel/cooking.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel/cooking.ml')

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