From ed04b8eb07ca3925af852c30a75c553c134f7d72 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 29 Oct 2018 17:56:10 +0100
Subject: Local universes for opaque polymorphic constants.

---
 kernel/declareops.ml | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

(limited to 'kernel/declareops.ml')

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 } *)
 
-- 
cgit v1.2.3