Local universes for opaque polymorphic constants.

1 files changed, 9 insertions, 2 deletions

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 3ed599c538..90638be3ec 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -101,6 +101,7 @@ let subst_const_body sub cb =
         const_body_code =
           Option.map (Cemitcodes.subst_to_patch_subst sub) cb.const_body_code;
         const_universes = cb.const_universes;
+        const_private_poly_univs = cb.const_private_poly_univs;
         const_inline_code = cb.const_inline_code;
         const_typing_flags = cb.const_typing_flags }
 
@@ -126,14 +127,20 @@ let hcons_const_universes cbu =
   match cbu with
   | Monomorphic_const ctx -> 
     Monomorphic_const (Univ.hcons_universe_context_set ctx)
-  | Polymorphic_const ctx -> 
+  | Polymorphic_const ctx ->
     Polymorphic_const (Univ.hcons_abstract_universe_context ctx)
 
+let hcons_const_private_univs = function
+  | None -> None
+  | Some univs -> Some (Univ.hcons_universe_context_set univs)
+
 let hcons_const_body cb =
   { cb with
     const_body = hcons_const_def cb.const_body;
     const_type = Constr.hcons cb.const_type;
-    const_universes = hcons_const_universes cb.const_universes }
+    const_universes = hcons_const_universes cb.const_universes;
+    const_private_poly_univs = hcons_const_private_univs cb.const_private_poly_univs;
+  }
 
 (** {6 Inductive types } *)