Merge PR #10201: Remove access to indirect opaques in the kernel

Ack-by: SkySkimmer
Reviewed-by: ejgallego
Reviewed-by: gares
Reviewed-by: maximedenes

23 files changed, 159 insertions, 168 deletions

diff --git a/checker/check.ml b/checker/check.ml
index a2c8a0f25d..76f40dbac2 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -50,7 +50,7 @@ let pr_path sp =
 
 type compilation_unit_name = DirPath.t
 
-type seg_proofs = Constr.constr Future.computation array
+type seg_proofs = Constr.constr option array
 
 type library_t = {
   library_name : compilation_unit_name;
@@ -100,16 +100,7 @@ let access_opaque_table dp i =
   assert (i < Array.length t);
   t.(i)
 
-let access_opaque_univ_table dp i =
-  try
-    let t = LibraryMap.find dp !opaque_univ_tables in
-    assert (i < Array.length t);
-    Some t.(i)
-  with Not_found -> None
-
-let () =
-  Opaqueproof.set_indirect_opaque_accessor access_opaque_table;
-  Opaqueproof.set_indirect_univ_accessor access_opaque_univ_table
+let () = Mod_checking.set_indirect_accessor access_opaque_table
 
 let check_one_lib admit senv (dir,m) =
   let md = m.library_compiled in
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 1dd16f1630..1cf07e7cc7 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -8,6 +8,14 @@ open Environ
 
 (** {6 Checking constants } *)
 
+let get_proof = ref (fun _ _ -> assert false)
+let set_indirect_accessor f = get_proof := f
+
+let indirect_accessor = {
+  Opaqueproof.access_proof = (fun dp n -> !get_proof dp n);
+  Opaqueproof.access_constraints = (fun _ _ -> assert false);
+}
+
 let check_constant_declaration env kn cb =
   Flags.if_verbose Feedback.msg_notice (str "  checking cst:" ++ Constant.print kn);
   (* Locally set the oracle for further typechecking *)
@@ -29,10 +37,16 @@ let check_constant_declaration env kn cb =
   in
   let ty = cb.const_type in
   let _ = infer_type env' ty 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)
+  in
   let () =
-    match Environ.body_of_constant_body env cb with
+    match body with
     | Some bd ->
-      let j = infer env' (fst bd) in
+      let j = infer env' bd in
       (try conv_leq env' j.uj_type ty
        with NotConvertible -> Type_errors.error_actual_type env j ty)
     | None -> ()
diff --git a/checker/mod_checking.mli b/checker/mod_checking.mli
index 6cff3e6b8c..dbc81c8507 100644
--- a/checker/mod_checking.mli
+++ b/checker/mod_checking.mli
@@ -8,4 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+val set_indirect_accessor : (Names.DirPath.t -> int -> Constr.t option) -> unit
+
 val check_module : Environ.env -> Names.ModPath.t -> Declarations.module_body -> unit
diff --git a/checker/values.ml b/checker/values.ml
index 5cbf0ff298..4b651cafb6 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -53,7 +53,6 @@ let v_enum name n = Sum(name,n,[||])
 let v_pair v1 v2 = v_tuple "*" [|v1; v2|]
 let v_bool = v_enum "bool" 2
 let v_unit = v_enum "unit" 1
-let v_ref v = v_tuple "ref" [|v|]
 
 let v_set v =
   let rec s = Sum ("Set.t",1,
@@ -70,13 +69,6 @@ let v_hmap vk vd = v_map Int (v_map vk vd)
 
 let v_pred v = v_pair v_bool (v_set v)
 
-(* lib/future *)
-let v_computation f =
-  Annot ("Future.computation",
-  v_ref
-    (v_sum "Future.comput" 0
-      [| [| Fail "Future.ongoing" |]; [| f |] |]))
-
 (** kernel/names *)
 
 let v_id = String
@@ -391,6 +383,6 @@ let v_libsum =
 let v_lib =
   Tuple ("library",[|v_compiled_lib;v_libraryobjs|])
 
-let v_opaques = Array (v_computation v_constr)
+let v_opaques = Array (Opt v_constr)
 let v_univopaques =
-  Opt (Tuple ("univopaques",[|Array (v_computation v_context_set);v_context_set;v_bool|]))
+  Opt (Tuple ("univopaques",[|Array (Opt v_context_set);v_context_set;v_bool|]))
diff --git a/dev/ci/user-overlays/10201-ppedrot-opaque-future-cleanup.sh b/dev/ci/user-overlays/10201-ppedrot-opaque-future-cleanup.sh
new file mode 100644
index 0000000000..e3bbb84bcb
--- /dev/null
+++ b/dev/ci/user-overlays/10201-ppedrot-opaque-future-cleanup.sh
@@ -0,0 +1,15 @@
+if [ "$CI_PULL_REQUEST" = "10201" ] || [ "$CI_BRANCH" = "opaque-future-cleanup" ]; then
+
+    coq_dpdgraph_CI_REF=opaque-future-cleanup
+    coq_dpdgraph_CI_GITURL=https://github.com/ppedrot/coq-dpdgraph
+
+    coqhammer_CI_REF=opaque-future-cleanup
+    coqhammer_CI_GITURL=https://github.com/ppedrot/coqhammer
+
+    elpi_CI_REF=opaque-future-cleanup
+    elpi_CI_GITURL=https://github.com/ppedrot/coq-elpi
+
+    paramcoq_CI_REF=opaque-future-cleanup
+    paramcoq_CI_GITURL=https://github.com/ppedrot/paramcoq
+
+fi
diff --git a/doc/plugin_tutorial/tuto1/src/simple_print.ml b/doc/plugin_tutorial/tuto1/src/simple_print.ml
index cfc38ff9c9..22a0163fbb 100644
--- a/doc/plugin_tutorial/tuto1/src/simple_print.ml
+++ b/doc/plugin_tutorial/tuto1/src/simple_print.ml
@@ -11,7 +11,7 @@ let simple_body_access gref =
     failwith "constructors are not covered in this example"
   | Globnames.ConstRef cst ->
     let cb = Environ.lookup_constant cst (Global.env()) in
-    match Global.body_of_constant_body cb with
+    match Global.body_of_constant_body Library.indirect_accessor cb with
     | Some(e, _) -> e
     | None -> failwith "This term has no value"
 
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 05f342a82a..c47bde0864 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -483,16 +483,6 @@ let constant_value_and_type env (kn, u) =
   in
   b', subst_instance_constr u cb.const_type, cst
 
-let body_of_constant_body env cb =
-  let otab = opaque_tables env in
-  match cb.const_body with
-  | Undef _ | Primitive _ ->
-     None
-  | Def c ->
-     Some (Mod_subst.force_constr c, Declareops.constant_polymorphic_context cb)
-  | OpaqueDef o ->
-     Some (Opaqueproof.force_proof otab o, Declareops.constant_polymorphic_context cb)
-
 (* These functions should be called under the invariant that [env] 
    already contains the constraints corresponding to the constant 
    application. *)
diff --git a/kernel/environ.mli b/kernel/environ.mli
index f6cd41861e..2abcea148a 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -215,12 +215,6 @@ val constant_value_and_type : env -> Constant.t puniverses ->
     polymorphic *)
 val constant_context : env -> Constant.t -> Univ.AUContext.t
 
-(** 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 : env -> Opaqueproof.opaque constant_body -> (Constr.constr * Univ.AUContext.t) option
-
 (* These functions should be called under the invariant that [env] 
    already contains the constraints corresponding to the constant 
    application. *)
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 18c1bcc0f8..75f96da3eb 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -16,6 +16,11 @@ open Mod_subst
 type work_list = (Instance.t * Id.t array) Cmap.t * 
   (Instance.t * Id.t array) Mindmap.t
 
+type indirect_accessor = {
+  access_proof : DirPath.t -> int -> constr option;
+  access_constraints : DirPath.t -> int -> Univ.ContextSet.t option;
+}
+
 type cooking_info = { 
   modlist : work_list; 
   abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t }
@@ -36,20 +41,8 @@ let empty_opaquetab = {
   opaque_dir = DirPath.initial;
 }
 
-(* hooks *)
-let default_get_opaque dp _ =
-  CErrors.user_err Pp.(pr_sequence str ["Cannot access opaque proofs in library"; DirPath.to_string dp])
-let default_get_univ dp _ =
-  CErrors.user_err (Pp.pr_sequence Pp.str [
-    "Cannot access universe constraints of opaque proofs in library ";
-    DirPath.to_string dp])
-
-let get_opaque = ref default_get_opaque
-let get_univ = ref default_get_univ
-
-let set_indirect_opaque_accessor f = (get_opaque := f)
-let set_indirect_univ_accessor f = (get_univ := f)
-(* /hooks *)
+let not_here () =
+  CErrors.user_err Pp.(str "Cannot access opaque delayed proof")
 
 let create cu = Direct ([],cu)
 
@@ -95,51 +88,52 @@ let join_opaque ?except { opaque_val = prfs; opaque_dir = odp; _ } = function
         let fp = snd (Int.Map.find i prfs) in
         join except fp
 
-let force_proof { opaque_val = prfs; opaque_dir = odp; _ } = function
+let force_proof access { opaque_val = prfs; opaque_dir = odp; _ } = function
   | Direct (_,cu) ->
       fst(Future.force cu)
   | Indirect (l,dp,i) ->
       let pt =
         if DirPath.equal dp odp
         then Future.chain (snd (Int.Map.find i prfs)) fst
-        else !get_opaque dp i in
+        else match access.access_proof dp i with
+        | None -> not_here ()
+        | Some v -> Future.from_val v
+      in
       let c = Future.force pt in
       force_constr (List.fold_right subst_substituted l (from_val c))
 
-let force_constraints { opaque_val = prfs; opaque_dir = odp; _ } = function
+let force_constraints access { opaque_val = prfs; opaque_dir = odp; _ } = function
   | Direct (_,cu) -> snd(Future.force cu)
   | Indirect (_,dp,i) ->
       if DirPath.equal dp odp
       then snd (Future.force (snd (Int.Map.find i prfs)))
-      else match !get_univ dp i with
+      else match access.access_constraints dp i with
         | None -> Univ.ContextSet.empty
-        | Some u -> Future.force u
+        | Some u -> u
 
-let get_constraints { opaque_val = prfs; opaque_dir = odp; _ } = function
-  | Direct (_,cu) -> Some(Future.chain cu snd)
-  | Indirect (_,dp,i) ->
-      if DirPath.equal dp odp
-      then Some(Future.chain (snd (Int.Map.find i prfs)) snd)
-      else !get_univ dp i
+let get_direct_constraints = function
+| Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.")
+| Direct (_, cu) -> Future.chain cu snd
 
 module FMap = Future.UUIDMap
 
-let a_constr = Future.from_val (mkRel 1)
-let a_univ = Future.from_val Univ.ContextSet.empty
-let a_discharge : cooking_info list = []
-
-let dump { opaque_val = otab; opaque_len = n; _ } =
-  let opaque_table = Array.make n a_constr in
-  let univ_table = Array.make n a_univ in
-  let disch_table = Array.make n a_discharge in
+let dump ?(except = Future.UUIDSet.empty) { opaque_val = otab; opaque_len = n; _ } =
+  let opaque_table = Array.make n None in
+  let univ_table = Array.make n None in
+  let disch_table = Array.make n [] in
   let f2t_map = ref FMap.empty in
-  Int.Map.iter (fun n (d,cu) ->
-    let c, u = Future.split2 cu in
-    Future.sink u;
-    Future.sink c;
-    opaque_table.(n) <- c;
-    univ_table.(n) <- u;
-    disch_table.(n) <- d;
-    f2t_map := FMap.add (Future.uuid cu) n !f2t_map)
-  otab;
+  let iter n (d, cu) =
+    let uid = Future.uuid cu in
+    let () = f2t_map := FMap.add (Future.uuid cu) n !f2t_map in
+    if Future.is_val cu then
+      let (c, u) = Future.force cu in
+      let () = univ_table.(n) <- Some u in
+      opaque_table.(n) <- Some c
+    else if Future.UUIDSet.mem uid except then
+      disch_table.(n) <- d
+    else
+      CErrors.anomaly
+        Pp.(str"Proof object "++int n++str" is not checked nor to be checked")
+  in
+  let () = Int.Map.iter iter otab in
   opaque_table, univ_table, disch_table, !f2t_map
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 4e8956af06..4646206e55 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -35,12 +35,20 @@ val create : proofterm -> opaque
   used so far *)
 val turn_indirect : DirPath.t -> opaque -> opaquetab -> opaque * opaquetab
 
+type indirect_accessor = {
+  access_proof : DirPath.t -> int -> constr option;
+  access_constraints : DirPath.t -> int -> Univ.ContextSet.t option;
+}
+(** When stored indirectly, opaque terms are indexed by their library
+    dirpath and an integer index. The two functions above activate
+    this indirect storage, by telling how to retrieve terms.
+*)
+
 (** From a [opaque] back to a [constr]. This might use the
-    indirect opaque accessor configured below. *)
-val force_proof : opaquetab -> opaque -> constr
-val force_constraints : opaquetab -> opaque -> Univ.ContextSet.t
-val get_constraints :
-  opaquetab -> opaque -> Univ.ContextSet.t Future.computation option
+    indirect opaque accessor given as an argument. *)
+val force_proof : indirect_accessor -> opaquetab -> opaque -> constr
+val force_constraints : indirect_accessor -> opaquetab -> opaque -> Univ.ContextSet.t
+val get_direct_constraints : opaque -> Univ.ContextSet.t Future.computation
 
 val subst_opaque : substitution -> opaque -> opaque
 
@@ -60,21 +68,8 @@ val discharge_direct_opaque :
 
 val join_opaque : ?except:Future.UUIDSet.t -> opaquetab -> opaque -> unit
 
-val dump : opaquetab ->
-  Constr.t Future.computation array *
-  Univ.ContextSet.t Future.computation array *
+val dump : ?except:Future.UUIDSet.t -> opaquetab ->
+  Constr.t option array *
+  Univ.ContextSet.t option array *
   cooking_info list array *
   int Future.UUIDMap.t
-
-(** When stored indirectly, opaque terms are indexed by their library
-    dirpath and an integer index. The following two functions activate
-    this indirect storage, by telling how to store and retrieve terms.
-    Default creator always returns [None], preventing the creation of
-    any indirect link, and default accessor always raises an error.
-*)
-
-val set_indirect_opaque_accessor :
-  (DirPath.t -> int -> constr Future.computation) -> unit
-val set_indirect_univ_accessor :
-  (DirPath.t -> int -> Univ.ContextSet.t Future.computation option) -> unit
-
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index a5d8a480ee..873cc2a172 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -458,19 +458,11 @@ let labels_of_mib mib =
   Array.iter visit_mip mib.mind_packets;
   get ()
 
-let globalize_constant_universes env cb =
+let globalize_constant_universes cb =
   match cb.const_universes with
   | Monomorphic cstrs ->
-    Now (false, cstrs) ::
-    (match cb.const_body with
-     | (Undef _ | Def _ | Primitive _) -> []
-     | OpaqueDef lc ->
-       match Opaqueproof.get_constraints (Environ.opaque_tables env) lc with
-       | None -> []
-       | Some fc ->
-            match Future.peek_val fc with
-             | None -> [Later fc]
-             | Some c -> [Now (false, c)])
+    (* Constraints hidden in the opaque body are added by [add_constant_aux] *)
+    [Now (false, cstrs)]
   | Polymorphic _ ->
     [Now (true, Univ.ContextSet.empty)]
       
@@ -480,9 +472,9 @@ let globalize_mind_universes mb =
     [Now (false, ctx)]
   | Polymorphic _ -> [Now (true, Univ.ContextSet.empty)]
 
-let constraints_of_sfb env sfb = 
+let constraints_of_sfb sfb =
   match sfb with
-  | SFBconst cb -> globalize_constant_universes env cb
+  | SFBconst cb -> globalize_constant_universes cb
   | SFBmind mib -> globalize_mind_universes mib
   | SFBmodtype mtb -> [Now (false, mtb.mod_constraints)]
   | SFBmodule mb -> [Now (false, mb.mod_constraints)]
@@ -520,7 +512,8 @@ let add_field ?(is_include=false) ((l,sfb) as field) gn senv =
          separately. *)
       senv
     else
-      let cst = constraints_of_sfb senv.env sfb in
+      (* Delayed constraints from opaque body are added by [add_constant_aux] *)
+      let cst = constraints_of_sfb sfb in
       add_constraints_list cst senv
   in
   let env' = match sfb, gn with
@@ -553,6 +546,15 @@ type exported_private_constant =
 
 let add_constant_aux ~in_section senv (kn, cb) =
   let l = Constant.label kn in
+  let delayed_cst = match cb.const_body with
+  | OpaqueDef o when not (Declareops.constant_is_polymorphic cb) ->
+    let fc = Opaqueproof.get_direct_constraints o in
+    begin match Future.peek_val fc with
+    | None -> [Later fc]
+    | Some c -> [Now (false, c)]
+    end
+  | Undef _ | Def _ | Primitive _ | OpaqueDef _ -> []
+  in
   let cb, otab = match cb.const_body with
     | OpaqueDef lc when not in_section ->
       (* In coqc, opaque constants outside sections will be stored
@@ -565,6 +567,7 @@ let add_constant_aux ~in_section senv (kn, cb) =
   in
   let senv = { senv with env = Environ.set_opaque_tables senv.env otab } in
   let senv' = add_field (l,SFBconst cb) (C kn) senv in
+  let senv' = add_constraints_list delayed_cst senv' in
   let senv'' = match cb.const_body with
     | Undef (Some lev) ->
       update_resolver
diff --git a/library/global.ml b/library/global.ml
index 58e2380440..d5ffae7716 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -132,9 +132,20 @@ let exists_objlabel id = Safe_typing.exists_objlabel id (safe_env ())
 
 let opaque_tables () = Environ.opaque_tables (env ())
 
-let body_of_constant_body ce = body_of_constant_body (env ()) ce
-
-let body_of_constant cst = body_of_constant_body (lookup_constant cst)
+let body_of_constant_body access env cb =
+  let open Declarations in
+  let otab = Environ.opaque_tables env in
+  match cb.const_body with
+  | Undef _ | Primitive _ ->
+     None
+  | Def c ->
+     Some (Mod_subst.force_constr c, Declareops.constant_polymorphic_context cb)
+  | OpaqueDef o ->
+     Some (Opaqueproof.force_proof access otab o, Declareops.constant_polymorphic_context cb)
+
+let body_of_constant_body access ce = body_of_constant_body access (env ()) ce
+
+let body_of_constant access cst = body_of_constant_body access (lookup_constant cst)
 
 (** Operations on kernel names *)
 
diff --git a/library/global.mli b/library/global.mli
index 984d8c666c..aa9fc18477 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -100,13 +100,13 @@ val mind_of_delta_kn : KerName.t -> MutInd.t
 
 val opaque_tables : unit -> Opaqueproof.opaquetab
 
-val body_of_constant : Constant.t -> (Constr.constr * Univ.AUContext.t) option
+val body_of_constant : Opaqueproof.indirect_accessor -> Constant.t -> (Constr.constr * 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.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 * 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 9f4eb531ed..039124635e 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -276,8 +276,8 @@ let in_import_library : DirPath.t list * bool -> obj =
 (** Delayed / available tables of opaque terms *)
 
 type 'a table_status =
-  | ToFetch of 'a Future.computation array delayed
-  | Fetched of 'a Future.computation array
+  | ToFetch of 'a option array delayed
+  | Fetched of 'a option array
 
 let opaque_tables =
   ref (LibraryMap.empty : (Constr.constr table_status) LibraryMap.t)
@@ -315,12 +315,13 @@ let access_opaque_table dp i =
 let access_univ_table dp i =
   try
     let what = "universe contexts of opaque proofs" in
-    Some (access_table what univ_tables dp i)
+    access_table what univ_tables dp i
   with Not_found -> None
 
-let () =
-  Opaqueproof.set_indirect_opaque_accessor access_opaque_table;
-  Opaqueproof.set_indirect_univ_accessor access_univ_table
+let indirect_accessor = {
+  Opaqueproof.access_proof = access_opaque_table;
+  Opaqueproof.access_constraints = access_univ_table;
+}
 
 (************************************************************************)
 (* Internalise libraries *)
@@ -328,9 +329,9 @@ let () =
 type seg_sum = summary_disk
 type seg_lib = library_disk
 type seg_univ = (* true = vivo, false = vi *)
-  Univ.ContextSet.t Future.computation array * Univ.ContextSet.t * bool
+  Univ.ContextSet.t option array * Univ.ContextSet.t * bool
 type seg_discharge = Opaqueproof.cooking_info list array
-type seg_proofs = Constr.constr Future.computation array
+type seg_proofs = Constr.constr option array
 
 let mk_library sd md digests univs =
   {
@@ -590,7 +591,7 @@ let save_library_to ?todo ~output_native_objects dir f otab =
         List.fold_left (fun e (r,_) -> Future.UUIDSet.add r.Stateid.uuid e)
           Future.UUIDSet.empty l in
   let cenv, seg, ast = Declaremods.end_library ~output_native_objects ~except dir in
-  let opaque_table, univ_table, disch_table, f2t_map = Opaqueproof.dump otab in
+  let opaque_table, univ_table, disch_table, f2t_map = Opaqueproof.dump ~except otab in
   let tasks, utab, dtab =
     match todo with
     | None -> None, None, None
@@ -603,16 +604,6 @@ let save_library_to ?todo ~output_native_objects dir f otab =
         Some (tasks,rcbackup),
         Some (univ_table,Univ.ContextSet.empty,false),
         Some disch_table in
-  let except =
-    Future.UUIDSet.fold (fun uuid acc ->
-      try Int.Set.add (Future.UUIDMap.find uuid f2t_map) acc
-      with Not_found -> acc)
-      except Int.Set.empty in
-  let is_done_or_todo i x = Future.is_val x || Int.Set.mem i except in
-  Array.iteri (fun i x ->
-    if not(is_done_or_todo i x) then CErrors.user_err ~hdr:"library"
-      Pp.(str"Proof object "++int i++str" is not checked nor to be checked"))
-    opaque_table;
   let sd = {
     md_name = dir;
     md_deps = Array.of_list (current_deps ());
diff --git a/library/library.mli b/library/library.mli
index f3186d847f..2c0673c3b1 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -34,9 +34,9 @@ val require_library_from_dirpath
 type seg_sum
 type seg_lib
 type seg_univ = (* cst, all_cst, finished? *)
-  Univ.ContextSet.t Future.computation array * Univ.ContextSet.t * bool
+  Univ.ContextSet.t option array * Univ.ContextSet.t * bool
 type seg_discharge = Opaqueproof.cooking_info list array
-type seg_proofs = Constr.constr Future.computation array
+type seg_proofs = Constr.constr option array
 
 (** Open a module (or a library); if the boolean is true then it's also
    an export otherwise just a simple import *)
@@ -73,3 +73,6 @@ val overwrite_library_filenames : string -> unit
 
 (** {6 Native compiler. } *)
 val native_name_from_filename : string -> string
+
+(** {6 Opaque accessors} *)
+val indirect_accessor : Opaqueproof.indirect_accessor
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 9db7c8d8d3..051d1f8e0f 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 (Environ.opaque_tables env) c)
+    (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 cffe8a3e78..f2b9ba2ec6 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 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 const with
+      match Global.body_of_constant Library.indirect_accessor const with
 	| Some (body, _) ->
           let env = Global.env () in
           let sigma = Evd.from_env env in
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index f51c6dc6be..2c107d39d9 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -413,7 +413,7 @@ let get_funs_constant mp =
   in
   function const ->
     let find_constant_body const =
-      match Global.body_of_constant const with
+      match Global.body_of_constant Library.indirect_accessor const with
 	| Some (body, _) ->
 	    let body = Tacred.cbv_norm_flags
 	      (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index ce7d149ae1..a6b088de0c 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -851,7 +851,7 @@ let make_graph ~pstate (f_ref : GlobRef.t) =
       end
     | _ -> raise (UserError (None, str "Not a function reference") )
   in
-  (match Global.body_of_constant_body c_body with
+  (match Global.body_of_constant_body Library.indirect_accessor c_body with
      | None -> error "Cannot build a graph over an axiom!"
      | Some (body, _) ->
        let env = Global.env () in
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 9541ea5882..fca33a24bf 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -549,7 +549,7 @@ let print_instance sigma cb =
 				
 let print_constant with_values sep sp udecl =
   let cb = Global.lookup_constant sp in
-  let val_0 = Global.body_of_constant_body cb in
+  let val_0 = Global.body_of_constant_body Library.indirect_accessor cb in
   let typ = cb.const_type in
   let univs =
     let open Univ in
@@ -557,7 +557,7 @@ let print_constant with_values sep sp udecl =
     match cb.const_body with
     | Undef _ | Def _ | Primitive _ -> cb.const_universes
     | OpaqueDef o ->
-      let body_uctxs = Opaqueproof.force_constraints otab o in
+      let body_uctxs = Opaqueproof.force_constraints Library.indirect_accessor otab o in
       match cb.const_universes with
       | Monomorphic ctx ->
         Monomorphic (ContextSet.union body_uctxs ctx)
@@ -717,7 +717,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 (Global.opaque_tables ()) lc)
+                str "Proof " ++ pr_lconstr_env env sigma (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/stm/stm.ml b/stm/stm.ml
index d469994f3f..660dc27211 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1837,22 +1837,18 @@ end = struct (* {{{ *)
         let o = match c.Declarations.const_body with
           | Declarations.OpaqueDef o -> o
           | _ -> assert false in
-        let uc =
-          Option.get
-            (Opaqueproof.get_constraints (Global.opaque_tables ()) o) in
+        (* No need to delay the computation, the future has been forced by
+           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
         (* We only manipulate monomorphic terms here. *)
         let map (c, ctx) = assert (Univ.AUContext.is_empty ctx); c in
-        let pr =
-          Future.from_val (map (Option.get (Global.body_of_constant_body c))) in
-        let uc =
-          Future.chain uc Univ.hcons_universe_context_set in
-        let pr = Future.chain pr discharge in
-        let pr = Future.chain pr Constr.hcons in
-        Future.sink pr;
-        let extra = Future.join uc in
-        u.(bucket) <- uc;
-        p.(bucket) <- pr;
-        u, Univ.ContextSet.union cst extra, false
+        let pr = map (Option.get (Global.body_of_constant_body Library.indirect_accessor c)) in
+        let pr = discharge pr in
+        let pr = Constr.hcons pr in
+        u.(bucket) <- Some uc;
+        p.(bucket) <- Some pr;
+        u, Univ.ContextSet.union cst uc, false
 
   let check_task name l i =
     match check_task_aux "" name l i with
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index 445f10ecc1..9353ef3902 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 (lookup_constant kn)) in
+  let body () = Option.map fst (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 (lookup_constant kn)) in
+        let body () = Option.map fst (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 317cf487cc..740b9031cc 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -57,7 +57,7 @@ let retrieve_first_recthm uctx = function
       let uctx = UState.context uctx in
       let inst = Univ.UContext.instance uctx in
       let map (c, ctx) = Vars.subst_instance_constr inst c in
-      (Option.map map (Global.body_of_constant_body cb), is_opaque cb)
+      (Option.map map (Global.body_of_constant_body Library.indirect_accessor cb), is_opaque cb)
   | _ -> assert false
 
 let adjust_guardness_conditions const = function