aboutsummaryrefslogtreecommitdiff
path: root/kernel/declareops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/declareops.ml')
-rw-r--r--kernel/declareops.ml3
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