diff options
| author | Pierre-Marie Pédrot | 2020-02-05 15:39:17 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-02-05 17:00:04 +0100 |
| commit | 5f508021585c3b385e603524b49a25ecc65cfa7d (patch) | |
| tree | c190c6b509b411a1aee3e030871acbe58469805e /kernel/declarations.ml | |
| parent | 2e273828c23fc50d924b1f3c3006fb2e9dc7d05b (diff) | |
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.
Diffstat (limited to 'kernel/declarations.ml')
| -rw-r--r-- | kernel/declarations.ml | 1 |
1 files changed, 1 insertions, 0 deletions
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 = |