From 5316d205993bb3fe3f69e8984fe53d4d50aa8d2a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 4 Jun 2019 13:44:05 +0200
Subject: Allow to delay polymorphic opaque constants.

We had to move the private opaque constraints out of the constant declaration
into the opaque table. The API is not very pretty yet due to a pervasive
confusion between monomorphic global constraints and polymorphic local ones,
but once we get rid of futures in the kernel this should be magically solved.
---
 checker/check.ml                               |  7 +--
 checker/mod_checking.ml                        | 23 +++++----
 checker/values.ml                              |  6 ++-
 doc/plugin_tutorial/tuto1/src/simple_print.ml  |  2 +-
 kernel/cooking.ml                              | 18 ++++----
 kernel/cooking.mli                             |  4 +-
 kernel/declarations.ml                         |  1 -
 kernel/declareops.ml                           |  6 ---
 kernel/modops.ml                               |  1 -
 kernel/opaqueproof.ml                          | 64 ++++++++++++++++++--------
 kernel/opaqueproof.mli                         | 17 +++++--
 kernel/safe_typing.ml                          | 38 +++++++++------
 kernel/term_typing.ml                          | 40 ++++++++--------
 library/global.ml                              |  9 +++-
 library/global.mli                             |  7 ++-
 library/library.ml                             |  9 ++--
 library/library.mli                            |  2 +-
 plugins/extraction/extraction.ml               |  2 +-
 plugins/funind/functional_principles_proofs.ml |  4 +-
 plugins/funind/functional_principles_types.ml  |  2 +-
 plugins/funind/indfun.ml                       |  2 +-
 printing/prettyp.ml                            | 12 +++--
 printing/printmod.ml                           |  2 +-
 stm/stm.ml                                     |  8 +++-
 vernac/assumptions.ml                          |  4 +-
 vernac/lemmas.ml                               |  2 +-
 26 files changed, 172 insertions(+), 120 deletions(-)

diff --git a/checker/check.ml b/checker/check.ml
index 903258daef..89cb834a4a 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -51,7 +51,7 @@ let pr_path sp =
 type compilation_unit_name = DirPath.t
 
 type seg_univ = Univ.ContextSet.t * bool
-type seg_proofs = (Opaqueproof.cooking_info list * int * Constr.constr option) array
+type seg_proofs = Opaqueproof.opaque_proofterm array
 
 type library_t = {
   library_name : compilation_unit_name;
@@ -98,10 +98,7 @@ let access_opaque_table dp i =
     with Not_found -> assert false
   in
   assert (i < Array.length t);
-  let (info, n, c) = t.(i) in
-  match c with
-  | None -> None
-  | Some c -> Some (Cooking.cook_constr info n c)
+  t.(i)
 
 let access_discharge = Cooking.cook_constr
 
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 0684623a81..7e49e741ad 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -31,16 +31,19 @@ let check_constant_declaration env kn cb =
   in
   let ty = cb.const_type in
   let _ = infer_type env' ty in
-  let env' = match cb.const_private_poly_univs, (cb.const_body, poly) with
-    | None, _ -> env'
-    | Some local, (OpaqueDef _, true) -> push_subgraph local env'
-    | Some _, _ -> assert false
-  in
-  let otab = Environ.opaque_tables env in
-  let body = match cb.const_body with
-  | Undef _ | Primitive _ -> None
-  | Def c -> Some (Mod_subst.force_constr c)
-  | OpaqueDef o -> Some (Opaqueproof.force_proof !indirect_accessor otab o)
+  let otab = Environ.opaque_tables env' in
+  let body, env' = match cb.const_body with
+  | Undef _ | Primitive _ -> None, env'
+  | Def c -> Some (Mod_subst.force_constr c), env'
+  | OpaqueDef o ->
+    let c, u = Opaqueproof.force_proof !indirect_accessor otab o in
+    let env' = match u, cb.const_universes with
+    | Opaqueproof.PrivateMonomorphic (), Monomorphic _ -> env'
+    | Opaqueproof.PrivatePolymorphic local, Polymorphic _ ->
+      push_subgraph local env'
+    | _ -> assert false
+    in
+    Some c, env'
   in
   let () =
     match body with
diff --git a/checker/values.ml b/checker/values.ml
index 4a4c8d803c..7b869cd130 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -230,7 +230,6 @@ let v_cb = v_tuple "constant_body"
     v_relevance;
     Any;
     v_univs;
-    Opt v_context_set;
     v_bool;
     v_typing_flags|]
 
@@ -399,6 +398,9 @@ let v_abstract =
 let v_cooking_info =
   Tuple ("cooking_info", [|v_work_list; v_abstract|])
 
-let v_opaques = Array (Tuple ("opaque", [| List v_cooking_info; Int; Opt v_constr |]))
+let v_delayed_universes =
+  Sum ("delayed_universes", 0, [| [| v_unit |]; [| v_context_set |] |])
+
+let v_opaques = Array (Tuple ("opaque", [| List v_cooking_info; Int; Opt (v_pair v_constr v_delayed_universes) |]))
 let v_univopaques =
   Opt (Tuple ("univopaques",[|v_context_set;v_bool|]))
diff --git a/doc/plugin_tutorial/tuto1/src/simple_print.ml b/doc/plugin_tutorial/tuto1/src/simple_print.ml
index 48b5f2214c..ba989b1bac 100644
--- a/doc/plugin_tutorial/tuto1/src/simple_print.ml
+++ b/doc/plugin_tutorial/tuto1/src/simple_print.ml
@@ -12,6 +12,6 @@ let simple_body_access gref =
   | Globnames.ConstRef cst ->
     let cb = Environ.lookup_constant cst (Global.env()) in
     match Global.body_of_constant_body Library.indirect_accessor cb with
-    | Some(e, _) -> EConstr.of_constr e
+    | Some(e, _, _) -> EConstr.of_constr e
     | None -> failwith "This term has no value"
 
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 1336e3e8bf..fbc0822570 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -159,7 +159,6 @@ type 'opaque result = {
   cook_body : (constr Mod_subst.substituted, 'opaque) constant_def;
   cook_type : types;
   cook_universes : universes;
-  cook_private_univs : Univ.ContextSet.t option;
   cook_relevance : Sorts.relevance;
   cook_inline : inline;
   cook_context : Constr.named_context option;
@@ -202,7 +201,7 @@ let lift_univs cb subst auctx0 =
     let subst, auctx = discharge_abstract_universe_context subst auctx0 auctx in
     subst, (Polymorphic auctx)
 
-let cook_constr { Opaqueproof.modlist ; abstract } (univs, c) =
+let cook_constr { Opaqueproof.modlist ; abstract } (univs, (c, priv)) =
   let cache = RefTable.create 13 in
   let abstract, usubst, abs_ctx = abstract in
   let ainst = Instance.of_array (Array.init univs Level.var) in
@@ -211,7 +210,15 @@ let cook_constr { Opaqueproof.modlist ; abstract } (univs, c) =
   let hyps = Context.Named.map expmod abstract in
   let hyps = abstract_context hyps in
   let c = abstract_constant_body (expmod c) hyps in
-  univs + AUContext.size abs_ctx, c
+  let priv = match priv with
+  | Opaqueproof.PrivateMonomorphic () ->
+    let () = assert (AUContext.is_empty abs_ctx) in
+    priv
+  | Opaqueproof.PrivatePolymorphic ctx ->
+    let ctx = on_snd (Univ.subst_univs_level_constraints (Univ.make_instance_subst usubst)) ctx in
+    Opaqueproof.PrivatePolymorphic ctx
+  in
+  univs + AUContext.size abs_ctx, (c, priv)
 
 let cook_constr infos univs c =
   let fold info (univs, c) = cook_constr info (univs, c) in
@@ -240,15 +247,10 @@ let cook_constant { from = cb; info } =
 		  hyps)
       hyps0 ~init:cb.const_hyps in
   let typ = abstract_constant_type (expmod cb.const_type) hyps in
-  let private_univs = Option.map (on_snd (Univ.subst_univs_level_constraints
-                                            (Univ.make_instance_subst usubst)))
-      cb.const_private_poly_univs
-  in
   {
     cook_body = body;
     cook_type = typ;
     cook_universes = univs;
-    cook_private_univs = private_univs;
     cook_relevance = cb.const_relevance;
     cook_inline = cb.const_inline_code;
     cook_context = Some const_hyps;
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 934b7c6b50..c98fb0bc3a 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -21,14 +21,14 @@ type 'opaque result = {
   cook_body : (constr Mod_subst.substituted, 'opaque) constant_def;
   cook_type : types;
   cook_universes : universes;
-  cook_private_univs : Univ.ContextSet.t option;
   cook_relevance : Sorts.relevance;
   cook_inline : inline;
   cook_context : Constr.named_context option;
 }
 
 val cook_constant : recipe -> Opaqueproof.opaque result
-val cook_constr : Opaqueproof.cooking_info list -> int -> constr -> constr
+val cook_constr : Opaqueproof.cooking_info list -> int ->
+  (constr * unit Opaqueproof.delayed_universes) -> (constr * unit Opaqueproof.delayed_universes)
 
 val cook_inductive :
   Opaqueproof.cooking_info -> mutual_inductive_body -> Entries.mutual_inductive_entry
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 388b4f14bf..deb01589b6 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -94,7 +94,6 @@ type 'opaque constant_body = {
     const_relevance : Sorts.relevance;
     const_body_code : Cemitcodes.to_patch_substituted option;
     const_universes : universes;
-    const_private_poly_univs : Univ.ContextSet.t option;
     const_inline_code : bool;
     const_typing_flags : typing_flags; (** The typing options which
                                            were used for
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index de9a052096..a8ebed2326 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -113,7 +113,6 @@ 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_relevance = cb.const_relevance;
         const_inline_code = cb.const_inline_code;
         const_typing_flags = cb.const_typing_flags }
@@ -144,16 +143,11 @@ let hcons_universes cbu =
   | Polymorphic ctx ->
     Polymorphic (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_universes cb.const_universes;
-    const_private_poly_univs = hcons_const_private_univs cb.const_private_poly_univs;
   }
 
 (** {6 Inductive types } *)
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 472fddb829..fcd88fd543 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -329,7 +329,6 @@ let strengthen_const mp_from l cb resolver =
     let u = Univ.make_abstract_instance (Declareops.constant_polymorphic_context cb) in
       { cb with
         const_body = Def (Mod_subst.from_val (mkConstU (con,u)));
-        const_private_poly_univs = None;
 	const_body_code = Some (Cemitcodes.from_val (Cbytegen.compile_alias con)) }
 
 let rec strengthen_mod mp_from mp_to mb =
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
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 6e275649cd..20c862c651 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -21,7 +21,11 @@ open Mod_subst
     When it is [turn_indirect] the data is relocated to an opaque table
     and the [opaque] is turned into an index. *)
 
-type proofterm = (constr * Univ.ContextSet.t) Future.computation
+type 'a delayed_universes =
+| PrivateMonomorphic of 'a
+| PrivatePolymorphic of Univ.ContextSet.t
+
+type proofterm = (constr * Univ.ContextSet.t delayed_universes) Future.computation
 type opaquetab
 type opaque
 
@@ -42,9 +46,12 @@ type cooking_info = {
   modlist : work_list;
   abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.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);
 }
 (** When stored indirectly, opaque terms are indexed by their library
     dirpath and an integer index. The two functions above activate
@@ -53,7 +60,7 @@ type indirect_accessor = {
 
 (** From a [opaque] back to a [constr]. This might use the
     indirect opaque accessor given as an argument. *)
-val force_proof : indirect_accessor -> opaquetab -> opaque -> constr
+val force_proof : indirect_accessor -> opaquetab -> opaque -> constr * unit delayed_universes
 val force_constraints : indirect_accessor -> opaquetab -> opaque -> Univ.ContextSet.t
 val get_direct_constraints : opaque -> Univ.ContextSet.t Future.computation
 
@@ -65,5 +72,5 @@ val discharge_direct_opaque :
 val join_opaque : ?except:Future.UUIDSet.t -> opaquetab -> opaque -> unit
 
 val dump : ?except:Future.UUIDSet.t -> opaquetab ->
-  (cooking_info list * int * Constr.t option) array *
+  opaque_proofterm array *
   int Future.UUIDMap.t
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 0b0f14eee7..596fcd210c 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -725,11 +725,14 @@ let export_side_effects mb env (b_ctx, eff) =
               let kn = eff.seff_constant in
                let ce = constant_entry_of_side_effect eff in
                let cb = Term_typing.translate_constant Term_typing.Pure env kn ce in
-               let map cu =
+              let map cu =
                 let (c, u) = Future.force cu in
-                let () = assert (Univ.ContextSet.is_empty u) in
+                let () = match u with
+                | Opaqueproof.PrivateMonomorphic ctx | Opaqueproof.PrivatePolymorphic ctx ->
+                  assert (Univ.ContextSet.is_empty ctx)
+                in
                 c
-               in
+              in
                let cb = map_constant map cb in
                let eff = { eff with seff_body = cb } in
                (push_seff env eff, export_eff eff)
@@ -742,13 +745,16 @@ let export_side_effects mb env (b_ctx, eff) =
      in
        translate_seff trusted seff [] env
 
-let n_univs cb = match cb.const_universes with
-| Monomorphic _ -> 0
-| Polymorphic auctx -> Univ.AUContext.size auctx
-
 let export_private_constants ~in_section ce senv =
   let exported, ce = export_side_effects senv.revstruct senv.env ce in
-  let map (kn, cb) = (kn, map_constant (fun p -> Opaqueproof.create ~univs:(n_univs cb) (Future.from_val (p, Univ.ContextSet.empty))) cb) in
+  let map univs p =
+    let univs, local = match univs with
+    | Monomorphic _ -> 0, Opaqueproof.PrivateMonomorphic Univ.ContextSet.empty
+    | Polymorphic auctx -> Univ.AUContext.size auctx, Opaqueproof.PrivatePolymorphic Univ.ContextSet.empty
+    in
+    Opaqueproof.create ~univs (Future.from_val (p, local))
+  in
+  let map (kn, cb) = (kn, map_constant (fun c -> map cb.const_universes c) cb) in
   let bodies = List.map map exported in
   let exported = List.map (fun (kn, _) -> kn) exported in
   let senv = List.fold_left (add_constant_aux ~in_section) senv bodies in
@@ -775,7 +781,11 @@ let add_constant (type a) ~(side_effect : a effect_entry) ~in_section l decl sen
         Term_typing.translate_constant Term_typing.Pure senv.env kn ce
     in
   let senv =
-    let cb = map_constant (fun c -> Opaqueproof.create ~univs:(n_univs cb) c) cb in
+    let univs = match cb.const_universes with
+    | Monomorphic _ -> 0
+    | Polymorphic auctx -> Univ.AUContext.size auctx
+    in
+    let cb = map_constant (fun c -> Opaqueproof.create ~univs c) cb in
     add_constant_aux ~in_section senv (kn, cb) in
   let senv =
     match decl with
@@ -791,14 +801,16 @@ let add_constant (type a) ~(side_effect : a effect_entry) ~in_section l decl sen
     | (Primitive _ | Undef _) -> assert false
     | Def c -> (Def c, cb.const_universes)
     | OpaqueDef o ->
-      let (b, ctx) = Future.force o in
-      match cb.const_universes with
-      | Monomorphic ctx' ->
+      let (b, delayed) = Future.force o in
+      match cb.const_universes, delayed with
+      | Monomorphic ctx', Opaqueproof.PrivateMonomorphic ctx ->
         OpaqueDef b, Monomorphic (Univ.ContextSet.union ctx ctx')
-      | Polymorphic auctx ->
+      | Polymorphic auctx, Opaqueproof.PrivatePolymorphic ctx ->
         (* Upper layers enforce that there are no internal constraints *)
         let () = assert (Univ.ContextSet.is_empty ctx) in
         OpaqueDef b, Polymorphic auctx
+      | (Monomorphic _ | Polymorphic _), (Opaqueproof.PrivateMonomorphic _ | Opaqueproof.PrivatePolymorphic _) ->
+        assert false
     in
     let cb = { cb with const_body = body; const_universes = univs } in
     let from_env = CEphemeron.create senv.revstruct in
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index f984088f47..9ec3269375 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -79,7 +79,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
         Cooking.cook_body = Undef nl;
         cook_type = t;
         cook_universes = univs;
-        cook_private_univs = None;
         cook_relevance = r;
         cook_inline = false;
         cook_context = ctx;
@@ -108,7 +107,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
       { Cooking.cook_body = cd;
         cook_type = ty;
         cook_universes = Monomorphic uctxt;
-        cook_private_univs = None;
         cook_inline = false;
         cook_context = None;
         cook_relevance = Sorts.Relevant;
@@ -124,7 +122,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
       let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c in
       let tyj = Typeops.infer_type env typ in
       let proofterm =
-        Future.chain body (fun ((body,uctx),side_eff) ->
+        Future.chain body begin fun ((body,uctx),side_eff) ->
           (* don't redeclare universes which are declared for the type *)
           let uctx = Univ.ContextSet.diff uctx univs in
           let j, uctx = match trust with
@@ -145,13 +143,13 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
           in
           let c = j.uj_val in
           feedback_completion_typecheck feedback_id;
-          c, uctx) in
+          c, Opaqueproof.PrivateMonomorphic uctx
+      end in
       let def = OpaqueDef proofterm in
       {
         Cooking.cook_body = def;
         cook_type = tyj.utj_val;
         cook_universes = Monomorphic univs;
-        cook_private_univs = None;
         cook_relevance = Sorts.relevance_of_sort tyj.utj_type;
         cook_inline = c.const_entry_inline_code;
         cook_context = c.const_entry_secctx;
@@ -168,8 +166,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
       let tj = Typeops.infer_type env typ in
       let sbst, auctx = Univ.abstract_universes nas uctx in
       let usubst = Univ.make_instance_subst sbst in
-      let (def, private_univs) =
-        let (body, ctx), side_eff = Future.join body in
+      let proofterm = Future.chain body begin fun ((body, ctx), side_eff) ->
         let body, ctx = match trust with
         | Pure -> body, ctx
         | SideEffects handle ->
@@ -183,16 +180,15 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
         let j = Typeops.infer env body in
         let _ = Typeops.judge_of_cast env j DEFAULTcast tj in
         let def = Vars.subst_univs_level_constr usubst j.uj_val in
-        def, private_univs
-      in
-      let def = OpaqueDef (Future.from_val (def, Univ.ContextSet.empty)) in
+        let () = feedback_completion_typecheck feedback_id in
+        def, Opaqueproof.PrivatePolymorphic private_univs
+      end in
+      let def = OpaqueDef proofterm in
       let typ = Vars.subst_univs_level_constr usubst tj.utj_val in
-        feedback_completion_typecheck feedback_id;
       {
         Cooking.cook_body = def;
         cook_type = typ;
         cook_universes = Polymorphic auctx;
-        cook_private_univs = Some private_univs;
         cook_relevance = Sorts.relevance_of_sort tj.utj_type;
         cook_inline = c.const_entry_inline_code;
         cook_context = c.const_entry_secctx;
@@ -211,22 +207,22 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
         body, ctx
       | SideEffects _ -> assert false
       in
-      let env, usubst, univs, private_univs = match c.const_entry_universes with
+      let env, usubst, univs = match c.const_entry_universes with
       | Monomorphic_entry univs ->
         let ctx = Univ.ContextSet.union univs ctx in
         let env = push_context_set ~strict:true ctx env in
-        env, Univ.empty_level_subst, Monomorphic ctx, None
+        env, Univ.empty_level_subst, Monomorphic ctx
       | Polymorphic_entry (nas, uctx) ->
         (** [ctx] must contain local universes, such that it has no impact
             on the rest of the graph (up to transitivity). *)
         let env = push_context ~strict:false uctx env in
         let sbst, auctx = Univ.abstract_universes nas uctx in
         let sbst = Univ.make_instance_subst sbst in
-        let env, local =
-          if Univ.ContextSet.is_empty ctx then env, None
-          else CErrors.anomaly Pp.(str "Local universes in non-opaque polymorphic definition.")
+        let () =
+          if not (Univ.ContextSet.is_empty ctx) then
+            CErrors.anomaly Pp.(str "Local universes in non-opaque polymorphic definition.")
         in
-        env, sbst, Polymorphic auctx, local
+        env, sbst, Polymorphic auctx
       in
       let j = Typeops.infer env body in
       let typ = match typ with
@@ -244,7 +240,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
         Cooking.cook_body = def;
         cook_type = typ;
         cook_universes = univs;
-        cook_private_univs = private_univs;
         cook_relevance = Retypeops.relevance_of_term env j.uj_val;
         cook_inline = c.const_entry_inline_code;
         cook_context = c.const_entry_secctx;
@@ -341,7 +336,6 @@ let build_constant_declaration env result =
     const_type = typ;
     const_body_code = tps;
     const_universes = univs;
-    const_private_poly_univs = result.cook_private_univs;
     const_relevance = result.cook_relevance;
     const_inline_code = result.cook_inline;
     const_typing_flags = Environ.typing_flags env }
@@ -368,7 +362,6 @@ let translate_recipe env _kn r =
     const_type = result.cook_type;
     const_body_code = tps;
     const_universes = univs;
-    const_private_poly_univs = result.cook_private_univs;
     const_relevance = result.cook_relevance;
     const_inline_code = result.cook_inline;
     const_typing_flags = Environ.typing_flags env }
@@ -407,7 +400,10 @@ let translate_local_def env _id centry =
     let (p, cst) = Future.force o in
     (** Let definitions are ensured to have no extra constraints coming from
         the body by virtue of the typing of [Entries.section_def_entry]. *)
-    let () = assert (Univ.ContextSet.is_empty cst) in
+    let () = match cst with
+    | Opaqueproof.PrivateMonomorphic ctx -> assert (Univ.ContextSet.is_empty ctx)
+    | Opaqueproof.PrivatePolymorphic ctx -> assert (Univ.ContextSet.is_empty ctx)
+    in
     p
   | Undef _ | Primitive _ -> assert false
   in
diff --git a/library/global.ml b/library/global.ml
index 3f30a63808..44e4a9b7e1 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -139,9 +139,14 @@ let body_of_constant_body access env cb =
   | Undef _ | Primitive _ ->
      None
   | Def c ->
-     Some (Mod_subst.force_constr c, Declareops.constant_polymorphic_context cb)
+    let u = match cb.const_universes with
+    | Monomorphic _ -> Opaqueproof.PrivateMonomorphic ()
+    | Polymorphic _ -> Opaqueproof.PrivatePolymorphic Univ.ContextSet.empty
+    in
+    Some (Mod_subst.force_constr c, u, Declareops.constant_polymorphic_context cb)
   | OpaqueDef o ->
-     Some (Opaqueproof.force_proof access otab o, Declareops.constant_polymorphic_context cb)
+    let c, u = Opaqueproof.force_proof access otab o in
+    Some (c, u, Declareops.constant_polymorphic_context cb)
 
 let body_of_constant_body access ce = body_of_constant_body access (env ()) ce
 
diff --git a/library/global.mli b/library/global.mli
index c36cec3511..34b6c52833 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -100,13 +100,16 @@ val mind_of_delta_kn : KerName.t -> MutInd.t
 
 val opaque_tables : unit -> Opaqueproof.opaquetab
 
-val body_of_constant : Opaqueproof.indirect_accessor -> Constant.t -> (Constr.constr * Univ.AUContext.t) option
+val body_of_constant : Opaqueproof.indirect_accessor -> Constant.t ->
+  (Constr.constr * unit Opaqueproof.delayed_universes * Univ.AUContext.t) option
 (** Returns the body of the constant if it has any, and the polymorphic context
     it lives in. For monomorphic constant, the latter is empty, and for
     polymorphic constants, the term contains De Bruijn universe variables that
     need to be instantiated. *)
 
-val body_of_constant_body : Opaqueproof.indirect_accessor -> Opaqueproof.opaque Declarations.constant_body -> (Constr.constr * Univ.AUContext.t) option
+val body_of_constant_body : Opaqueproof.indirect_accessor ->
+  Opaqueproof.opaque Declarations.constant_body ->
+    (Constr.constr * unit Opaqueproof.delayed_universes * Univ.AUContext.t) option
 (** Same as {!body_of_constant} but on {!Declarations.constant_body}. *)
 
 (** {6 Compiled libraries } *)
diff --git a/library/library.ml b/library/library.ml
index 1ac75d2fdc..a55fe33617 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -280,7 +280,7 @@ type 'a table_status =
   | Fetched of 'a array
 
 let opaque_tables =
-  ref (LibraryMap.empty : ((Opaqueproof.cooking_info list * int * Constr.constr option) table_status) LibraryMap.t)
+  ref (LibraryMap.empty : (Opaqueproof.opaque_proofterm table_status) LibraryMap.t)
 
 let add_opaque_table dp st =
   opaque_tables := LibraryMap.add dp st !opaque_tables
@@ -306,10 +306,7 @@ let access_table what tables dp i =
 
 let access_opaque_table dp i =
   let what = "opaque proofs" in
-  let (info, n, c) = access_table what opaque_tables dp i in
-  match c with
-  | None -> None
-  | Some c -> Some (Cooking.cook_constr info n c)
+  access_table what opaque_tables dp i
 
 let indirect_accessor = {
   Opaqueproof.access_proof = access_opaque_table;
@@ -323,7 +320,7 @@ type seg_sum = summary_disk
 type seg_lib = library_disk
 type seg_univ = (* true = vivo, false = vi *)
   Univ.ContextSet.t * bool
-type seg_proofs = (Opaqueproof.cooking_info list * int * Constr.t option) array
+type seg_proofs = Opaqueproof.opaque_proofterm array
 
 let mk_library sd md digests univs =
   {
diff --git a/library/library.mli b/library/library.mli
index 727eca10cf..de395fd3b4 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -35,7 +35,7 @@ type seg_sum
 type seg_lib
 type seg_univ = (* all_cst, finished? *)
   Univ.ContextSet.t * bool
-type seg_proofs = (Opaqueproof.cooking_info list * int * Constr.t option) array
+type seg_proofs = Opaqueproof.opaque_proofterm array
 
 (** Open a module (or a library); if the boolean is true then it's also
    an export otherwise just a simple import *)
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 051d1f8e0f..8c505eb202 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -115,7 +115,7 @@ let get_body lconstr = EConstr.of_constr (Mod_subst.force_constr lconstr)
 
 let get_opaque env c =
   EConstr.of_constr
-    (Opaqueproof.force_proof Library.indirect_accessor (Environ.opaque_tables env) c)
+    (fst (Opaqueproof.force_proof Library.indirect_accessor (Environ.opaque_tables env) c))
 
 let applistc c args = EConstr.mkApp (c, Array.of_list args)
 
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 17498c6384..ce3b5a82d6 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -951,7 +951,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
 (*   observe (str "rec_args_num := " ++ str (string_of_int (rec_args_num + 1) )); *)
   let f_def = Global.lookup_constant (fst (destConst evd f)) in
   let eq_lhs = mkApp(f,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i))) in
-  let (f_body, _) = Option.get (Global.body_of_constant_body Library.indirect_accessor f_def) in
+  let (f_body, _, _) = Option.get (Global.body_of_constant_body Library.indirect_accessor f_def) in
   let f_body = EConstr.of_constr f_body in
   let params,f_body_with_params = decompose_lam_n evd nb_params f_body in
   let (_,num),(_,_,bodies) = destFix evd f_body_with_params in
@@ -1082,7 +1082,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
     in
     let get_body const =
       match Global.body_of_constant Library.indirect_accessor const with
-        | Some (body, _) ->
+        | Some (body, _, _) ->
           let env = Global.env () in
           let sigma = Evd.from_env env in
              Tacred.cbv_norm_flags
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 8af5dc818b..53d303bb99 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -413,7 +413,7 @@ let get_funs_constant mp =
   function const ->
     let find_constant_body const =
       match Global.body_of_constant Library.indirect_accessor const with
-        | Some (body, _) ->
+        | Some (body, _, _) ->
             let body = Tacred.cbv_norm_flags
               (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
               (Global.env ())
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index ecf953bef1..0ecfbacb09 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -853,7 +853,7 @@ let make_graph (f_ref : GlobRef.t) =
   in
   (match Global.body_of_constant_body Library.indirect_accessor c_body with
      | None -> error "Cannot build a graph over an axiom!"
-     | Some (body, _) ->
+     | Some (body, _, _) ->
        let env = Global.env () in
          let extern_body,extern_type =
            with_full_print (fun () ->
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index f55bfb504f..396c954b42 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -583,11 +583,15 @@ let print_constant with_values sep sp udecl =
 	str"*** [ " ++
 	print_basename sp ++ print_instance sigma cb ++ str " : " ++ cut () ++ pr_ltype typ ++
 	str" ]" ++
-        Printer.pr_universes sigma univs ?priv:cb.const_private_poly_univs
-    | Some (c, ctx) ->
+        Printer.pr_universes sigma univs
+    | Some (c, priv, ctx) ->
+      let priv = match priv with
+      | Opaqueproof.PrivateMonomorphic () -> None
+      | Opaqueproof.PrivatePolymorphic ctx -> Some ctx
+      in
 	print_basename sp ++ print_instance sigma cb ++ str sep ++ cut () ++
 	(if with_values then print_typed_body env sigma (Some c,typ) else pr_ltype typ)++
-        Printer.pr_universes sigma univs ?priv:cb.const_private_poly_univs)
+        Printer.pr_universes sigma univs ?priv)
 
 let gallina_print_constant_with_infos sp udecl =
   print_constant true " = " sp udecl ++
@@ -723,7 +727,7 @@ let print_full_pure_context env sigma =
 	      | OpaqueDef lc ->
 		str "Theorem " ++ print_basename con ++ cut () ++
                 str " : " ++ pr_ltype_env env sigma typ ++ str "." ++ fnl () ++
-                str "Proof " ++ pr_lconstr_env env sigma (Opaqueproof.force_proof Library.indirect_accessor (Global.opaque_tables ()) lc)
+                str "Proof " ++ pr_lconstr_env env sigma (fst (Opaqueproof.force_proof Library.indirect_accessor (Global.opaque_tables ()) lc))
 	      | Def c ->
 		str "Definition " ++ print_basename con ++ cut () ++
                 str "  : " ++ pr_ltype_env env sigma typ ++ cut () ++ str " := " ++
diff --git a/printing/printmod.ml b/printing/printmod.ml
index bd97104f60..52a3616152 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -297,7 +297,7 @@ let print_body is_impl extent env mp (l,body) =
 		hov 2 (str ":= " ++
                        Printer.pr_lconstr_env env sigma (Mod_subst.force_constr l))
 	      | _ -> mt ()) ++ str "." ++
-            Printer.pr_abstract_universe_ctx sigma ctx ?priv:cb.const_private_poly_univs)
+            Printer.pr_abstract_universe_ctx sigma ctx)
     | SFBmind mib ->
       match extent with
       | WithContents ->
diff --git a/stm/stm.ml b/stm/stm.ml
index d77e37c910..bae51d1794 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1746,14 +1746,18 @@ end = struct (* {{{ *)
            the call to [check_task_aux] above. *)
         let uc = Opaqueproof.force_constraints Library.indirect_accessor (Global.opaque_tables ()) o in
         let uc = Univ.hcons_universe_context_set uc in
-        let (pr, ctx) = Option.get (Global.body_of_constant_body Library.indirect_accessor c) in
+        let (pr, priv, ctx) = Option.get (Global.body_of_constant_body Library.indirect_accessor c) in
         (* We only manipulate monomorphic terms here. *)
         let () = assert (Univ.AUContext.is_empty ctx) in
+        let () = match priv with
+        | Opaqueproof.PrivateMonomorphic () -> ()
+        | Opaqueproof.PrivatePolymorphic ctx -> assert (Univ.ContextSet.is_empty ctx)
+        in
         let pr = Constr.hcons pr in
         let (ci, univs, dummy) = p.(bucket) in
         let () = assert (Option.is_empty dummy) in
         let () = assert (Int.equal (Univ.AUContext.size ctx) univs) in
-        p.(bucket) <- ci, univs, Some pr;
+        p.(bucket) <- ci, univs, Some (pr, priv);
         Univ.ContextSet.union cst uc, false
 
   let check_task name l i =
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index 9353ef3902..5c6a282894 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -168,7 +168,7 @@ let rec traverse current ctx accu t = match Constr.kind t with
   let body () = id |> Global.lookup_named |> NamedDecl.get_value in
   traverse_object accu body (VarRef id)
 | Const (kn, _) ->
-  let body () = Option.map fst (Global.body_of_constant_body Library.indirect_accessor (lookup_constant kn)) in
+  let body () = Option.map pi1 (Global.body_of_constant_body Library.indirect_accessor (lookup_constant kn)) in
   traverse_object accu body (ConstRef kn)
 | Ind ((mind, _) as ind, _) ->
   traverse_inductive accu mind (IndRef ind)
@@ -181,7 +181,7 @@ let rec traverse current ctx accu t = match Constr.kind t with
     | Lambda(_,_,oty), Const (kn, _)
       when Vars.noccurn 1 oty &&
       not (Declareops.constant_has_body (lookup_constant kn)) ->
-        let body () = Option.map fst (Global.body_of_constant_body Library.indirect_accessor (lookup_constant kn)) in
+        let body () = Option.map pi1 (Global.body_of_constant_body Library.indirect_accessor (lookup_constant kn)) in
         traverse_object
           ~inhabits:(current,ctx,Vars.subst1 mkProp oty) accu body (ConstRef kn)
     | _ ->
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 7aba64fb93..cd8b17f681 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -93,7 +93,7 @@ let retrieve_first_recthm uctx = function
       (* we get the right order somehow but surely it could be enforced in a better way *)
       let uctx = UState.context uctx in
       let inst = Univ.UContext.instance uctx in
-      let map (c, ctx) = Vars.subst_instance_constr inst c in
+      let map (c, _, _) = Vars.subst_instance_constr inst c in
       (Option.map map (Global.body_of_constant_body Library.indirect_accessor cb), is_opaque cb)
   | _ -> assert false
 
-- 
cgit v1.2.3