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/declarations.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'kernel/declarations.ml') 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 = -- cgit v1.2.3