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/declareops.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/declareops.ml')
| -rw-r--r-- | kernel/declareops.ml | 3 |
1 files changed, 2 insertions, 1 deletions
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 |