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/indTyping.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/indTyping.ml')

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