diff options
| author | Gaëtan Gilbert | 2020-02-07 13:25:59 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-07 13:25:59 +0100 |
| commit | 633d9829d4e3678583c9e1ad161253fb53be1290 (patch) | |
| tree | 4c7edf5c090b369574b68d587787bac4b74d89ba /kernel/declareops.ml | |
| parent | adf04f62d3ff5b0651cec2e8596ce3900d3af1eb (diff) | |
| parent | 22b3b961804bea2c8b56cbab9a0c4902bf45c56c (diff) | |
Merge PR #11528: Checker does not rely on Monomorphic fields
Reviewed-by: SkySkimmer
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 |