1 files changed, 46 insertions, 18 deletions

diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index e18b726111..66c50c4b57 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -20,13 +20,24 @@ type cooking_info = {
   modlist : work_list;
   abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t }
 
+type 'a delayed_universes =
+| PrivateMonomorphic of 'a
+| PrivatePolymorphic of Univ.ContextSet.t
+
+type opaque_proofterm = cooking_info list * int * (Constr.t * unit delayed_universes) option
+
 type indirect_accessor = {
-  access_proof : DirPath.t -> int -> constr option;
-  access_discharge : cooking_info list -> int -> constr -> constr;
+  access_proof : DirPath.t -> int -> opaque_proofterm;
+  access_discharge : cooking_info list -> int -> (Constr.t * unit delayed_universes) -> (Constr.t * unit delayed_universes);
 }
 
-type proofterm = (constr * Univ.ContextSet.t) Future.computation
+let drop_mono = function
+| PrivateMonomorphic _ -> PrivateMonomorphic ()
+| PrivatePolymorphic _ as ctx -> ctx
+
+type proofterm = (constr * Univ.ContextSet.t delayed_universes) Future.computation
 type universes = int
+
 type opaque =
   | Indirect of substitution list * DirPath.t * int (* subst, lib, index *)
   | Direct of universes * cooking_info list * proofterm
@@ -59,7 +70,10 @@ let turn_indirect dp o tab = match o with
       hashconsing of their contents, potentially as a future. *)
       let hcons (c, u) =
         let c = Constr.hcons c in
-        let u = Univ.hcons_universe_context_set u in
+        let u = match u with
+        | PrivateMonomorphic u -> PrivateMonomorphic (Univ.hcons_universe_context_set u)
+        | PrivatePolymorphic u -> PrivatePolymorphic (Univ.hcons_universe_context_set u)
+        in
         (c, u)
       in
       let cu = Future.chain cu hcons in
@@ -97,34 +111,42 @@ let join_opaque ?except { opaque_val = prfs; opaque_dir = odp; _ } = function
 
 let force_proof access { opaque_val = prfs; opaque_dir = odp; _ } = function
   | Direct (n, d, cu) ->
-    let (c, _) = Future.force cu in
-    access.access_discharge d n c
+    let (c, u) = Future.force cu in
+    access.access_discharge d n (c, drop_mono u)
   | Indirect (l,dp,i) ->
-      let c =
+      let c, u =
         if DirPath.equal dp odp
         then
           let (n, d, cu) = Int.Map.find i prfs in
-          let (c, _) = Future.force cu in
-          access.access_discharge d n c
-        else match access.access_proof dp i with
-        | None -> not_here ()
-        | Some v -> v
+          let (c, u) = Future.force cu in
+          access.access_discharge d n (c, drop_mono u)
+        else
+          let (n, d, cu) = access.access_proof dp i in
+          match cu with
+          | None -> not_here ()
+          | Some (c, u) -> access.access_discharge n d (c, u)
       in
-      force_constr (List.fold_right subst_substituted l (from_val c))
+      let c = force_constr (List.fold_right subst_substituted l (from_val c)) in
+      (c, u)
+
+let get_mono (_, u) = match u with
+| PrivateMonomorphic ctx -> ctx
+| PrivatePolymorphic _ -> Univ.ContextSet.empty
 
 let force_constraints _access { opaque_val = prfs; opaque_dir = odp; _ } = function
   | Direct (_,_,cu) ->
-    snd(Future.force cu)
+    get_mono (Future.force cu)
   | Indirect (_,dp,i) ->
       if DirPath.equal dp odp
       then
         let (_, _, cu) = Int.Map.find i prfs in
-        snd (Future.force cu)
+        get_mono (Future.force cu)
       else Univ.ContextSet.empty
 
 let get_direct_constraints = function
 | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.")
-| Direct (_, _, cu) -> Future.chain cu snd
+| Direct (_, _, cu) ->
+  Future.chain cu get_mono
 
 module FMap = Future.UUIDMap
 
@@ -136,8 +158,14 @@ let dump ?(except = Future.UUIDSet.empty) { opaque_val = otab; opaque_len = n; _
     let () = f2t_map := FMap.add (Future.uuid cu) n !f2t_map in
     let c =
       if Future.is_val cu then
-        let (c, _) = Future.force cu in
-        Some c
+        let (c, priv) = Future.force cu in
+        let priv = match priv with
+        | PrivateMonomorphic _ ->
+          let () = assert (Int.equal univs 0) in
+          PrivateMonomorphic ()
+        | PrivatePolymorphic _ as priv -> priv
+        in
+        Some (c, priv)
       else if Future.UUIDSet.mem uid except then None
       else
         CErrors.anomaly