library/opaqueTables: enable their use in interactive mode

Before this patch opaque tables were only growing, making them unusable
in interactive mode (leak on Undo).

With this patch the opaque tables are functional and part of the env.
I.e. a constant_body can point to the proof term in 2 ways:
  1) directly (before the constant is discharged)
  2) indirectly, via an int, that is mapped by the opaque table to
     the proof term.
This is now consistent in batch/interactive mode

This is step 0 to make an interactive coqtop able to dump a .vo/.vi

34 files changed, 286 insertions, 250 deletions

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 5f6aebc4e..412742611 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -161,10 +161,10 @@ let on_body ml hy f = function
     OpaqueDef (Opaqueproof.discharge_direct_opaque ~cook_constr:f
                  { Opaqueproof.modlist = ml; abstract = hy } o)
 
-let constr_of_def = function
+let constr_of_def otab = function
   | Undef _ -> assert false
   | Def cs -> Mod_subst.force_constr cs
-  | OpaqueDef lc -> Opaqueproof.force_proof lc
+  | OpaqueDef lc -> Opaqueproof.force_proof otab lc
 
 let expmod_constr_subst cache modlist subst c =
   let c = expmod_constr cache modlist c in
@@ -189,7 +189,8 @@ let lift_univs cb subst =
       subst, Univ.UContext.make (inst,cstrs')
   else subst, cb.const_universes
 
-let cook_constant env { from = cb; info = { Opaqueproof.modlist; abstract } } =
+let cook_constant env { from = cb; info } =
+  let { Opaqueproof.modlist; abstract } = info in
   let cache = RefTable.create 13 in
   let abstract, usubst, abs_ctx = abstract in
   let usubst, univs = lift_univs cb usubst in
@@ -211,7 +212,7 @@ let cook_constant env { from = cb; info = { Opaqueproof.modlist; abstract } } =
     | TemplateArity (ctx,s) ->
   	let t = mkArity (ctx,Type s.template_level) in
   	let typ = abstract_constant_type (expmod t) hyps in
-  	let j = make_judge (constr_of_def body) typ in
+  	let j = make_judge (constr_of_def (opaque_tables env) body) typ in
   	Typeops.make_polymorphic_if_constant_for_ind env j
   in
   let projection pb =
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 51e435d79..d99382129 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -42,10 +42,10 @@ let instantiate cb c =
     Vars.subst_instance_constr (Univ.UContext.instance cb.const_universes) c
   else c
 
-let body_of_constant cb = match cb.const_body with
+let body_of_constant otab cb = match cb.const_body with
   | Undef _ -> None
   | Def c -> Some (instantiate cb (force_constr c))
-  | OpaqueDef o -> Some (instantiate cb (Opaqueproof.force_proof o))
+  | OpaqueDef o -> Some (instantiate cb (Opaqueproof.force_proof otab o))
 
 let type_of_constant cb =
   match cb.const_type with
@@ -54,23 +54,24 @@ let type_of_constant cb =
       if t' == t then x else RegularArity t'
   | TemplateArity _ as x -> x
 
-let constraints_of_constant cb = Univ.Constraint.union 
+let constraints_of_constant otab cb = Univ.Constraint.union 
   (Univ.UContext.constraints cb.const_universes)
   (match cb.const_body with
   | Undef _ -> Univ.empty_constraint
   | Def c -> Univ.empty_constraint
-  | OpaqueDef o -> Univ.ContextSet.constraints (Opaqueproof.force_constraints o))
+  | OpaqueDef o ->
+      Univ.ContextSet.constraints (Opaqueproof.force_constraints otab o))
 
-let universes_of_constant cb = 
+let universes_of_constant otab cb = 
   match cb.const_body with
   | Undef _ | Def _ -> cb.const_universes
   | OpaqueDef o -> 
     Univ.UContext.union cb.const_universes 
-      (Univ.ContextSet.to_context (Opaqueproof.force_constraints o))
+      (Univ.ContextSet.to_context (Opaqueproof.force_constraints otab o))
 
-let universes_of_polymorphic_constant cb = 
+let universes_of_polymorphic_constant otab cb = 
   if cb.const_polymorphic then 
-    let univs = universes_of_constant cb in
+    let univs = universes_of_constant otab cb in
       Univ.instantiate_univ_context univs
   else Univ.UContext.empty
 
@@ -291,9 +292,9 @@ let hcons_mind mib =
 
 (** {6 Stm machinery } *)
 
-let join_constant_body cb =
+let join_constant_body otab cb =
   match cb.const_body with
-  | OpaqueDef o -> Opaqueproof.join_opaque o
+  | OpaqueDef o -> Opaqueproof.join_opaque otab o
   | _ -> ()
 
 let string_of_side_effect = function
diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index 04a067aff..497856676 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -28,15 +28,19 @@ val constant_has_body : constant_body -> bool
 (** Accessing const_body, forcing access to opaque proof term if needed.
     Only use this function if you know what you're doing. *)
 
-val body_of_constant : constant_body -> Term.constr option
+val body_of_constant :
+  Opaqueproof.opaquetab -> constant_body -> Term.constr option
 val type_of_constant : constant_body -> constant_type
-val constraints_of_constant : constant_body -> Univ.constraints
-val universes_of_constant : constant_body -> Univ.universe_context
+val constraints_of_constant :
+  Opaqueproof.opaquetab -> constant_body -> Univ.constraints
+val universes_of_constant :
+  Opaqueproof.opaquetab -> constant_body -> Univ.universe_context
 
 (** Return the universe context, in case the definition is polymorphic, otherwise
     the context is empty. *)
 
-val universes_of_polymorphic_constant : constant_body -> Univ.universe_context
+val universes_of_polymorphic_constant :
+  Opaqueproof.opaquetab -> constant_body -> Univ.universe_context
 
 val is_opaque : constant_body -> bool
 
@@ -71,7 +75,7 @@ val subst_wf_paths : substitution -> wf_paths -> wf_paths
 
 val subst_mind_body : substitution -> mutual_inductive_body -> mutual_inductive_body
 
-val join_constant_body : constant_body -> unit
+val join_constant_body : Opaqueproof.opaquetab -> constant_body -> unit
 
 (** {6 Hash-consing} *)
 
diff --git a/kernel/environ.ml b/kernel/environ.ml
index b331d8da7..c3e59487c 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -57,6 +57,8 @@ let universes env = env.env_stratification.env_universes
 let named_context env = env.env_named_context
 let named_context_val env = env.env_named_context,env.env_named_vals
 let rel_context env = env.env_rel_context
+let opaque_tables env = env.indirect_pterms
+let set_opaque_tables env indirect_pterms = { env with indirect_pterms }
 
 let empty_context env =
   match env.env_rel_context, env.env_named_context with
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 5e9e5264d..a20944758 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -46,6 +46,9 @@ val rel_context   : env -> rel_context
 val named_context : env -> named_context
 val named_context_val : env -> named_context_val
 
+val opaque_tables : env -> Opaqueproof.opaquetab
+val set_opaque_tables : env -> Opaqueproof.opaquetab -> env
+
 
 val engagement    : env -> engagement option
 val is_impredicative_set : env -> bool
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index cab3276c3..7a9b12c43 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -72,7 +72,7 @@ let rec check_with_def env struc (idl,c) mp equiv =
       (* In the spirit of subtyping.check_constant, we accept
          any implementations of parameters and opaques terms,
 	 as long as they have the right type *)
-      let ccst = Declareops.constraints_of_constant cb in
+      let ccst = Declareops.constraints_of_constant (opaque_tables env) cb in
       let env' = Environ.add_constraints ccst env' in
       let c',cst = match cb.const_body with
 	| Undef _ | OpaqueDef _ ->
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 859f83e05..585b38a08 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -612,19 +612,20 @@ let clean_bounded_mod_expr sign =
 
 (** {6 Stm machinery } *)
 
-let rec join_module mb =
-  implem_iter join_signature join_expression mb.mod_expr;
-  Option.iter join_expression mb.mod_type_alg;
-  join_signature mb.mod_type
-and join_modtype mt =
-  Option.iter join_expression mt.typ_expr_alg;
-  join_signature mt.typ_expr
-and join_field (l,body) = match body with
-  |SFBconst sb -> join_constant_body sb
+let rec join_module otab mb =
+  implem_iter (join_signature otab) (join_expression otab) mb.mod_expr;
+  Option.iter (join_expression otab) mb.mod_type_alg;
+  join_signature otab mb.mod_type
+and join_modtype otab mt =
+  Option.iter (join_expression otab) mt.typ_expr_alg;
+  join_signature otab mt.typ_expr
+and join_field otab (l,body) = match body with
+  |SFBconst sb -> join_constant_body otab sb
   |SFBmind _ -> ()
-  |SFBmodule m -> join_module m
-  |SFBmodtype m -> join_modtype m
-and join_structure struc = List.iter join_field struc
-and join_signature sign = functor_iter join_modtype join_structure sign
-and join_expression me = functor_iter join_modtype (fun _ -> ()) me
+  |SFBmodule m -> join_module otab m
+  |SFBmodtype m -> join_modtype otab m
+and join_structure otab struc = List.iter (join_field otab) struc
+and join_signature otab sign =
+  functor_iter (join_modtype otab) (join_structure otab) sign
+and join_expression otab me = functor_iter (join_modtype otab) (fun _ -> ()) me
 
diff --git a/kernel/modops.mli b/kernel/modops.mli
index 63d71a566..0009b859c 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -80,8 +80,7 @@ val clean_bounded_mod_expr : module_signature -> module_signature
 
 (** {6 Stm machinery } *)
 
-val join_module : module_body -> unit
-val join_structure : structure_body -> unit
+val join_structure : Opaqueproof.opaquetab -> structure_body -> unit
 
 (** {6 Errors } *)
 
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index a5def3dc8..52e6eb95d 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -21,7 +21,8 @@ type proofterm = (constr * Univ.universe_context_set) Future.computation
 type opaque =
   | Indirect of substitution list * DirPath.t * int (* subst, lib, index *)
   | Direct of cooking_info list * proofterm
-  | NoIndirect of substitution list * proofterm
+type opaquetab = (cooking_info list * proofterm) Int.Map.t * DirPath.t
+let empty_opaquetab = Int.Map.empty, DirPath.initial
 
 (* hooks *)
 let default_get_opaque dp _ =
@@ -31,87 +32,113 @@ let default_get_univ dp _ =
   Errors.error
     ("Cannot access universe constraints of opaque proofs in library " ^
     DirPath.to_string dp)
-let default_mk_indirect _ = None
-let default_join_indirect_local_opaque _ _ = ()
-let default_join_indirect_local_univ _ _ = ()
 
 let get_opaque = ref default_get_opaque
 let get_univ = ref default_get_univ
-let join_indirect_local_opaque = ref default_join_indirect_local_opaque
-let join_indirect_local_univ = ref default_join_indirect_local_univ
-let mk_indirect = ref default_mk_indirect
 
 let set_indirect_opaque_accessor f = (get_opaque := f)
 let set_indirect_univ_accessor f = (get_univ := f)
-let set_indirect_creator f = (mk_indirect := f)
-let set_join_indirect_local_opaque f = join_indirect_local_opaque := f
-let set_join_indirect_local_univ f = join_indirect_local_univ := f
-let reset_indirect_creator () = mk_indirect := default_mk_indirect
 (* /hooks *)
 
 let create cu = Direct ([],cu)
 
-let turn_indirect o = match o with
-  | Indirect _
-  | NoIndirect _ -> Errors.anomaly (Pp.str "Already an indirect opaque")
+let turn_indirect dp o (prfs,odp) = match o with
+  | Indirect _ -> Errors.anomaly (Pp.str "Already an indirect opaque")
   | Direct (d,cu) ->
       let cu = Future.chain ~pure:true cu (fun (c, u) -> hcons_constr c, u) in
-      match !mk_indirect (d,cu) with
-      | None -> Future.sink cu; NoIndirect([],cu)
-      | Some (dp,i) -> Indirect ([],dp,i)
+      let id = Int.Map.cardinal prfs in
+      let prfs = Int.Map.add id (d,cu) prfs in
+      let ndp =
+        if DirPath.equal dp odp then odp
+        else if DirPath.equal odp DirPath.initial then dp
+        else Errors.anomaly
+          (Pp.str "Using the same opaque table for multiple dirpaths") in
+      Indirect ([],dp,id), (prfs, ndp)
 
 let subst_opaque sub = function
   | Indirect (s,dp,i) -> Indirect (sub::s,dp,i)
-  | NoIndirect (s,uc) -> NoIndirect (sub::s,uc)
   | Direct _ -> Errors.anomaly (Pp.str "Substituting a Direct opaque")
 
 let iter_direct_opaque f = function
-  | Indirect _
-  | NoIndirect _ -> Errors.anomaly (Pp.str "Not a direct opaque")
+  | Indirect _ -> Errors.anomaly (Pp.str "Not a direct opaque")
   | Direct (d,cu) ->
       Direct (d,Future.chain ~pure:true cu (fun (c, u) -> f c; c, u))
 
 let discharge_direct_opaque ~cook_constr ci = function
-  | Indirect _
-  | NoIndirect _ -> Errors.anomaly (Pp.str "Not a direct opaque")
+  | Indirect _ -> Errors.anomaly (Pp.str "Not a direct opaque")
   | Direct (d,cu) ->
       Direct (ci::d,Future.chain ~pure:true cu (fun (c, u) -> cook_constr c, u))
 
-let join_opaque = function
+let join_opaque (prfs,odp) = function
   | Direct (_,cu) -> ignore(Future.join cu)
-  | NoIndirect (_,cu) -> ignore(Future.join cu)
   | Indirect (_,dp,i) ->
-      !join_indirect_local_opaque dp i;
-      !join_indirect_local_univ dp i
+      if DirPath.equal dp odp then
+        let fp = snd (Int.Map.find i prfs) in
+        ignore(Future.join fp)
 
-let force_proof = function
+let uuid_opaque (prfs,odp) = function
+  | Direct (_,cu) -> Some (Future.uuid cu)
+  | Indirect (_,dp,i) ->
+      if DirPath.equal dp odp
+      then Some (Future.uuid (snd (Int.Map.find i prfs)))
+      else None
+
+let force_proof (prfs,odp) = function
   | Direct (_,cu) ->
       fst(Future.force cu)
-  | NoIndirect (l,cu) ->
-      let c, _ = Future.force cu in
-      force_constr (List.fold_right subst_substituted l (from_val c))
   | Indirect (l,dp,i) ->
-      let c = Future.force (!get_opaque dp i) in
+      let pt =
+        if DirPath.equal dp odp
+        then Future.chain ~pure:true (snd (Int.Map.find i prfs)) fst
+        else !get_opaque dp i in
+      let c = Future.force pt in
       force_constr (List.fold_right subst_substituted l (from_val c))
 
-let force_constraints = function
-  | Direct (_,cu)
-  | NoIndirect(_,cu) -> snd(Future.force cu)
+let force_constraints (prfs,odp) = function
+  | Direct (_,cu) -> snd(Future.force cu)
   | Indirect (_,dp,i) ->
-      match !get_univ dp i with
-      | None -> Univ.ContextSet.empty
-      | Some u -> Future.force u
-
-let get_constraints = function
-  | Direct (_,cu)
-  | NoIndirect(_,cu) -> Some(Future.chain ~pure:true cu snd)
-  | Indirect (_,dp,i) -> !get_univ dp i
+      if DirPath.equal dp odp
+      then snd (Future.force (snd (Int.Map.find i prfs)))
+      else match !get_univ dp i with
+        | None -> Univ.ContextSet.empty
+        | Some u -> Future.force u
+
+let get_constraints (prfs,odp) = function
+  | Direct (_,cu) -> Some(Future.chain ~pure:true cu snd)
+  | Indirect (_,dp,i) ->
+      if DirPath.equal dp odp
+      then Some(Future.chain ~pure:true (snd (Int.Map.find i prfs)) snd)
+      else !get_univ dp i
 
-let get_proof = function
+let get_proof (prfs,odp) = function
   | Direct (_,cu) -> Future.chain ~pure:true cu fst
-  | NoIndirect(l,cu) ->
-      Future.chain ~pure:true cu (fun (c,_) ->
-        force_constr (List.fold_right subst_substituted l (from_val c)))
   | Indirect (l,dp,i) ->
-      Future.chain ~pure:true (!get_opaque dp i) (fun c ->
+      let pt =
+        if DirPath.equal dp odp
+        then Future.chain ~pure:true (snd (Int.Map.find i prfs)) fst
+        else !get_opaque dp i in
+      Future.chain ~pure:true pt (fun c ->
         force_constr (List.fold_right subst_substituted l (from_val c)))
+ 
+module FMap = Future.UUIDMap
+
+let a_constr = Future.from_val (Term.mkRel 1)
+let a_univ = Future.from_val Univ.ContextSet.empty
+let a_discharge : cooking_info list = []
+
+let dump (otab,_) =
+  let n = Int.Map.cardinal otab in
+  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 f2t_map = ref FMap.empty in
+  Int.Map.iter (fun n (d,cu) ->
+    let c, u = Future.split2 ~greedy:true 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;
+  opaque_table, univ_table, disch_table, !f2t_map
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 092f0aeb1..5f1c28292 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -9,6 +9,7 @@
 open Names
 open Term
 open Mod_subst
+open Int
 
 (** This module implements the handling of opaque proof terms.
     Opauqe proof terms are special since:
@@ -20,20 +21,25 @@ open Mod_subst
     and the [opaque] is turned into an index. *)
 
 type proofterm = (constr * Univ.universe_context_set) Future.computation
+type opaquetab
 type opaque
 
+val empty_opaquetab : opaquetab
+
 (** From a [proofterm] to some [opaque]. *)
 val create : proofterm -> opaque
 
-(** Turn a direct [opaque] into an indirect one, also hashconses constr *)
-val turn_indirect : opaque -> opaque
+(** Turn a direct [opaque] into an indirect one, also hashconses constr.
+ *  The integer is an hint of the maximum id used so far *)
+val turn_indirect : DirPath.t -> opaque -> opaquetab -> opaque * opaquetab
 
 (** From a [opaque] back to a [constr]. This might use the
     indirect opaque accessor configured below. *)
-val force_proof : opaque -> constr
-val force_constraints : opaque -> Univ.universe_context_set
-val get_proof : opaque -> Term.constr Future.computation
-val get_constraints : opaque -> Univ.universe_context_set Future.computation option
+val force_proof : opaquetab -> opaque -> constr
+val force_constraints : opaquetab -> opaque -> Univ.universe_context_set
+val get_proof : opaquetab -> opaque -> Term.constr Future.computation
+val get_constraints :
+  opaquetab -> opaque -> Univ.universe_context_set Future.computation option
 
 val subst_opaque : substitution -> opaque -> opaque
 val iter_direct_opaque : (constr -> unit) -> opaque -> opaque
@@ -52,7 +58,14 @@ type cooking_info = {
 val discharge_direct_opaque :
   cook_constr:(constr -> constr) -> cooking_info -> opaque -> opaque
 
-val join_opaque : opaque -> unit
+val uuid_opaque : opaquetab -> opaque -> Future.UUID.t option
+val join_opaque : opaquetab -> opaque -> unit
+
+val dump : opaquetab ->
+  Constr.t Future.computation array *
+  Univ.universe_context_set Future.computation 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
@@ -61,12 +74,8 @@ val join_opaque : opaque -> unit
     any indirect link, and default accessor always raises an error.
 *)
 
-val set_indirect_creator :
-  (cooking_info list * proofterm -> (DirPath.t * int) option) -> unit
 val set_indirect_opaque_accessor :
   (DirPath.t -> int -> Term.constr Future.computation) -> unit
 val set_indirect_univ_accessor :
   (DirPath.t -> int -> Univ.universe_context_set Future.computation option) -> unit
-val set_join_indirect_local_opaque : (DirPath.t -> int -> unit) -> unit
-val set_join_indirect_local_univ : (DirPath.t -> int -> unit) -> unit
-val reset_indirect_creator : unit -> unit
+
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index a5221c779..48043f116 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -74,7 +74,9 @@ type env = {
   env_nb_rel        : int;
   env_stratification : stratification;
   env_conv_oracle   : Conv_oracle.oracle;
-  retroknowledge : Retroknowledge.retroknowledge }
+  retroknowledge : Retroknowledge.retroknowledge;
+  indirect_pterms : Opaqueproof.opaquetab;
+}
 
 type named_context_val = named_context * named_vals
 
@@ -96,7 +98,8 @@ let empty_env = {
     env_engagement = None;
     env_type_in_type = false};
   env_conv_oracle = Conv_oracle.empty;
-  retroknowledge = Retroknowledge.initial_retroknowledge }
+  retroknowledge = Retroknowledge.initial_retroknowledge;
+  indirect_pterms = Opaqueproof.empty_opaquetab }
 
 
 (* Rel context *)
@@ -141,7 +144,9 @@ let push_named d env =
     env_nb_rel = env.env_nb_rel;
     env_stratification = env.env_stratification;
     env_conv_oracle = env.env_conv_oracle;
-    retroknowledge = env.retroknowledge; }
+    retroknowledge = env.retroknowledge;
+    indirect_pterms = env.indirect_pterms;
+  }
 
 let lookup_named_val id env =
   snd(List.find (fun (id',_) -> Id.equal id id') env.env_named_vals)
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index 9561333c8..7ef2ab009 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -54,7 +54,9 @@ type env = {
     env_nb_rel        : int;
     env_stratification : stratification;
     env_conv_oracle   : Conv_oracle.oracle;
-    retroknowledge : Retroknowledge.retroknowledge }
+    retroknowledge : Retroknowledge.retroknowledge;
+    indirect_pterms : Opaqueproof.opaquetab;
+}
 
 type named_context_val = named_context * named_vals
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index f7464013f..9aca7727b 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -125,7 +125,7 @@ type safe_environment =
     type_in_type : bool;
     imports : vodigest DPMap.t;
     loads : (module_path * module_body) list;
-    local_retroknowledge : Retroknowledge.action list}
+    local_retroknowledge : Retroknowledge.action list }
 
 and modvariant =
   | NONE
@@ -133,6 +133,12 @@ and modvariant =
   | SIG of module_parameters * safe_environment (** saved env *)
   | STRUCT of module_parameters * safe_environment (** saved env *)
 
+let rec library_dp_of_senv senv =
+  match senv.modvariant with
+  | NONE | LIBRARY -> ModPath.dp senv.modpath
+  | SIG(_,senv) -> library_dp_of_senv senv
+  | STRUCT(_,senv) -> library_dp_of_senv senv
+
 let empty_environment =
   { env = Environ.empty_env;
     modpath = initial_path;
@@ -219,7 +225,7 @@ let is_curmod_library senv =
   match senv.modvariant with LIBRARY -> true | _ -> false
 
 let join_safe_environment e =
-  Modops.join_structure e.revstruct;
+  Modops.join_structure (Environ.opaque_tables e.env) e.revstruct;
   List.fold_left
     (fun e fc -> add_constraints (Now (Future.join fc)) e)
     {e with future_cst = []} e.future_cst
@@ -312,9 +318,12 @@ let push_named_def (id,de) senv =
   let c,typ,univs = Term_typing.translate_local_def senv.env id de in
   let senv' = push_context univs senv in
   let c, senv' = match c with
-    | Def c -> Mod_subst.force_constr c, senv' 
-    | OpaqueDef o -> Opaqueproof.force_proof o, 
-      push_context_set (Opaqueproof.force_constraints o) senv'
+    | Def c -> Mod_subst.force_constr c, senv'
+    | OpaqueDef o ->
+        Opaqueproof.force_proof (Environ.opaque_tables senv'.env) o,
+        push_context_set
+          (Opaqueproof.force_constraints (Environ.opaque_tables senv'.env) o)
+          senv'
     | _ -> assert false in
   let env'' = safe_push_named (id,Some c,typ) senv'.env in
     {senv' with env=env''}
@@ -341,7 +350,7 @@ let labels_of_mib mib =
   Array.iter visit_mip mib.mind_packets;
   get ()
 
-let globalize_constant_universes cb =
+let globalize_constant_universes env cb =
   if cb.const_polymorphic then
     [Now Univ.Constraint.empty]
   else
@@ -350,7 +359,7 @@ let globalize_constant_universes cb =
 	(match cb.const_body with
 	| (Undef _ | Def _) -> []
 	| OpaqueDef lc ->
-	  match Opaqueproof.get_constraints lc with
+	  match Opaqueproof.get_constraints (Environ.opaque_tables env) lc with
 	  | None -> []
 	  | Some fc ->
             match Future.peek_val fc with
@@ -363,9 +372,9 @@ let globalize_mind_universes mb =
   else
     [Now (Univ.UContext.constraints mb.mind_universes)]
 
-let constraints_of_sfb sfb = 
+let constraints_of_sfb env sfb = 
   match sfb with
-  | SFBconst cb -> globalize_constant_universes cb
+  | SFBconst cb -> globalize_constant_universes env cb
   | SFBmind mib -> globalize_mind_universes mib
   | SFBmodtype mtb -> [Now mtb.typ_constraints]
   | SFBmodule mb -> [Now mb.mod_constraints]
@@ -389,7 +398,7 @@ let add_field ((l,sfb) as field) gn senv =
     | SFBmodule _ | SFBmodtype _ ->
       check_modlabel l senv; (Label.Set.singleton l, Label.Set.empty)
   in
-  let cst = constraints_of_sfb sfb in
+  let cst = constraints_of_sfb senv.env sfb in
   let senv = add_constraints_list cst senv in
   let env' = match sfb, gn with
     | SFBconst cb, C con -> Environ.add_constant con cb senv.env
@@ -421,13 +430,17 @@ let add_constant dir l decl senv =
       let cb = Term_typing.translate_recipe senv.env kn r in
       if DirPath.is_empty dir then Declareops.hcons_const_body cb else cb
   in
-  let cb = match cb.const_body with
+  let cb, otab = match cb.const_body with
     | OpaqueDef lc when DirPath.is_empty dir ->
       (* In coqc, opaque constants outside sections will be stored
          indirectly in a specific table *)
-      { cb with const_body = OpaqueDef (Opaqueproof.turn_indirect lc) }
-    | _ -> cb
+      let od, otab =
+        Opaqueproof.turn_indirect
+          (library_dp_of_senv senv) lc (Environ.opaque_tables senv.env) in
+      { cb with const_body = OpaqueDef od }, otab
+    | _ -> cb, (Environ.opaque_tables senv.env)
   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'' = match cb.const_body with
     | Undef (Some lev) ->
@@ -588,7 +601,7 @@ let propagate_senv newdef newenv newresolver senv oldsenv =
     imports = senv.imports;
     loads = senv.loads@oldsenv.loads;
     local_retroknowledge =
-      senv.local_retroknowledge@oldsenv.local_retroknowledge }
+            senv.local_retroknowledge@oldsenv.local_retroknowledge }
 
 let end_module l restype senv =
   let mp = senv.modpath in
@@ -597,7 +610,7 @@ let end_module l restype senv =
   let () = check_empty_context senv in
   let mbids = List.rev_map fst params in
   let mb = build_module_body params restype senv in
-  let newenv = oldsenv.env in
+  let newenv = Environ.set_opaque_tables oldsenv.env (Environ.opaque_tables senv.env) in
   let newenv = set_engagement_opt newenv senv.engagement in
   let senv'=
     propagate_loads { senv with
@@ -619,7 +632,7 @@ let end_modtype l senv =
   let () = check_empty_context senv in
   let mbids = List.rev_map fst params in
   let auto_tb = NoFunctor (List.rev senv.revstruct) in
-  let newenv = oldsenv.env in
+  let newenv = Environ.set_opaque_tables oldsenv.env (Environ.opaque_tables senv.env) in
   let newenv = Environ.add_constraints senv.univ newenv in
   let newenv = set_engagement_opt newenv senv.engagement in
   let senv' = propagate_loads {senv with env=newenv} in
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 4f54220e7..857f577a8 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -352,7 +352,8 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
       let u1 = inductive_instance mind1 in
       let arity1,cst1 = constrained_type_of_inductive env 
 	((mind1,mind1.mind_packets.(i)),u1) in
-      let cst2 = Declareops.constraints_of_constant cb2 in 
+      let cst2 =
+        Declareops.constraints_of_constant (Environ.opaque_tables env) cb2 in 
       let typ2 = Typeops.type_of_constant_type env cb2.const_type in
       let cst = Constraint.union cst (Constraint.union cst1 cst2) in
       let error = NotConvertibleTypeField (env, arity1, typ2) in
@@ -367,7 +368,8 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
       if Declareops.constant_has_body cb2 then error DefinitionFieldExpected;
       let u1 = inductive_instance mind1 in
       let ty1,cst1 = constrained_type_of_constructor (cstr,u1) (mind1,mind1.mind_packets.(i)) in
-      let cst2 = Declareops.constraints_of_constant cb2 in
+      let cst2 =
+        Declareops.constraints_of_constant (Environ.opaque_tables env) cb2 in
       let ty2 = Typeops.type_of_constant_type env cb2.const_type in
       let cst = Constraint.union cst (Constraint.union cst1 cst2) in
       let error = NotConvertibleTypeField (env, ty1, ty2) in
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 232508bc8..415e91f70 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -86,7 +86,7 @@ let handle_side_effects env body side_eff =
 	      let univs = cb.const_universes in
 		sub_body c (Univ.UContext.instance univs) b 1 (Vars.lift 1 t)
       | OpaqueDef b -> 
-          let b = Opaqueproof.force_proof b in
+          let b = Opaqueproof.force_proof (opaque_tables env) b in
 	  let poly = cb.const_polymorphic in
 	    if not poly then
               let b_ty = Typeops.type_of_constant_type env cb.const_type in
@@ -217,9 +217,11 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
         | Undef _ -> Idset.empty
         | Def cs -> global_vars_set env (Mod_subst.force_constr cs)
         | OpaqueDef lc ->
-            let vars = global_vars_set env (Opaqueproof.force_proof lc) in
+            let vars =
+              global_vars_set env
+                (Opaqueproof.force_proof (opaque_tables env) lc) in
             (* we force so that cst are added to the env immediately after *)
-            ignore(Opaqueproof.force_constraints lc);
+            ignore(Opaqueproof.force_constraints (opaque_tables env) lc);
             !suggest_proof_using kn env vars ids_typ context_ids;
             if !Flags.compilation_mode = Flags.BuildVo then
               record_aux env ids_typ vars;
diff --git a/lib/future.ml b/lib/future.ml
index 77386a1a9..6ebbd4b1d 100644
--- a/lib/future.ml
+++ b/lib/future.ml
@@ -40,6 +40,8 @@ module UUID = struct
   let equal = (==)
 end
 
+module UUIDMap = Map.Make(UUID)
+
 type 'a assignement = [ `Val of 'a | `Exn of exn | `Comp of 'a computation]
 
 (* Val is not necessarily a final state, so the
diff --git a/lib/future.mli b/lib/future.mli
index c4b55db25..18b014132 100644
--- a/lib/future.mli
+++ b/lib/future.mli
@@ -60,6 +60,8 @@ module UUID : sig
   val equal : t -> t -> bool
 end
 
+module UUIDMap : Map.S with type key = UUID.t
+
 exception NotReady
 
 type 'a computation
diff --git a/library/assumptions.ml b/library/assumptions.ml
index e4638f5e4..b01e24196 100644
--- a/library/assumptions.ml
+++ b/library/assumptions.ml
@@ -236,7 +236,7 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st (* t *) =
           else (s, acc)
       else (s, acc)
     in
-      match Declareops.body_of_constant cb with
+      match Global.body_of_constant_body cb with
       | None -> do_type (Axiom kn)
       | Some body -> do_constr body s acc
 
diff --git a/library/declare.ml b/library/declare.ml
index 1c9e10a19..4ec81c49f 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -116,7 +116,7 @@ let open_constant i ((sp,kn), obj) =
     match (Global.lookup_constant con).const_body with
     | (Def _ | Undef _) -> ()
     | OpaqueDef lc ->
-        match Opaqueproof.get_constraints lc with
+        match Opaqueproof.get_constraints (Global.opaque_tables ())lc with
         | Some f when Future.is_val f -> Global.push_context_set (Future.force f)
         | _ -> ()
 
@@ -208,7 +208,8 @@ let declare_sideff env fix_exn se =
     match cb with
     | { const_body = Def sc } -> (Mod_subst.force_constr sc, Univ.ContextSet.empty), false
     | { const_body = OpaqueDef fc } -> 
-      (Opaqueproof.force_proof fc, Opaqueproof.force_constraints fc), true
+      (Opaqueproof.force_proof (Environ.opaque_tables env) fc,
+       Opaqueproof.force_constraints (Environ.opaque_tables env) fc), true
     | { const_body = Undef _ } -> anomaly(str"Undefined side effect")
   in
   let ty_of cb =
diff --git a/library/global.ml b/library/global.ml
index 80238d8e2..49f78e495 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -113,6 +113,14 @@ let lookup_modtype kn = lookup_modtype kn (env())
 
 let exists_objlabel id = Safe_typing.exists_objlabel id (safe_env ())
 
+let opaque_tables () = Environ.opaque_tables (env ())
+let body_of_constant_body cb = Declareops.body_of_constant (opaque_tables ()) cb
+let body_of_constant cst = body_of_constant_body (lookup_constant cst)
+let constraints_of_constant_body cb =
+  Declareops.constraints_of_constant (opaque_tables ()) cb
+let universes_of_constant_body cb =
+  Declareops.universes_of_constant (opaque_tables ()) cb
+
 (** Operations on kernel names *)
 
 let constant_of_delta_kn kn =
@@ -153,7 +161,9 @@ let type_of_global_unsafe r =
   | VarRef id -> Environ.named_type id env
   | ConstRef c -> 
      let cb = Environ.lookup_constant c env in 
-     let univs = Declareops.universes_of_polymorphic_constant cb in
+     let univs =
+       Declareops.universes_of_polymorphic_constant
+         (Environ.opaque_tables env) cb in
      let ty = Typeops.type_of_constant_type env cb.Declarations.const_type in
        Vars.subst_instance_constr (Univ.UContext.instance univs) ty
   | IndRef ind ->
@@ -175,7 +185,9 @@ let type_of_global_in_context env r =
   | VarRef id -> Environ.named_type id env, Univ.UContext.empty
   | ConstRef c -> 
      let cb = Environ.lookup_constant c env in 
-     let univs = Declareops.universes_of_polymorphic_constant cb in
+     let univs =
+       Declareops.universes_of_polymorphic_constant
+         (Environ.opaque_tables env) cb in
        Typeops.type_of_constant_type env cb.Declarations.const_type, univs
   | IndRef ind ->
      let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
@@ -198,7 +210,8 @@ let universes_of_global env r =
     | VarRef id -> Univ.UContext.empty
     | ConstRef c -> 
       let cb = Environ.lookup_constant c env in 
-	Declareops.universes_of_polymorphic_constant cb
+	Declareops.universes_of_polymorphic_constant
+          (Environ.opaque_tables env) cb
     | IndRef ind ->
       let (mib, oib) = Inductive.lookup_mind_specif env ind in
 	Univ.instantiate_univ_context mib.mind_universes 
diff --git a/library/global.mli b/library/global.mli
index 7dcfdbd3a..8ae77a9e4 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -87,6 +87,14 @@ val exists_objlabel  : Label.t -> bool
 val constant_of_delta_kn : kernel_name -> constant
 val mind_of_delta_kn : kernel_name -> mutual_inductive
 
+val opaque_tables : unit -> Opaqueproof.opaquetab
+val body_of_constant : constant -> Term.constr option
+val body_of_constant_body : Declarations.constant_body -> Term.constr option
+val constraints_of_constant_body :
+  Declarations.constant_body -> Univ.constraints
+val universes_of_constant_body :
+  Declarations.constant_body -> Univ.universe_context
+
 (** {6 Compiled libraries } *)
 
 val start_library : DirPath.t -> module_path
diff --git a/library/heads.ml b/library/heads.ml
index 8b28f0500..94ce11731 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -123,7 +123,7 @@ let compute_head = function
    let is_Def = function Declarations.Def _ -> true | _ -> false in
    let body = 
      if cb.Declarations.const_proj = None && is_Def cb.Declarations.const_body
-     then Declareops.body_of_constant cb else None 
+     then Declareops.body_of_constant (Environ.opaque_tables env) cb else None 
    in
      (match body with
      | None -> RigidHead (RigidParameter cst)
diff --git a/library/library.ml b/library/library.ml
index 7bff05cda..7f5ca5af6 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -351,87 +351,15 @@ let access_opaque_table dp i =
     (fetch_table "opaque proofs")
     add_opaque_table !opaque_tables dp i
 let access_univ_table dp i =
-  access_table
-    (fetch_table "universe contexts of opaque proofs")
-    add_univ_table !univ_tables dp i
-
-(** Table of opaque terms from the library currently being compiled *)
-
-module OpaqueTables = struct
-
- let a_constr = Future.from_val (Term.mkRel 1)
- let a_univ = Future.from_val Univ.ContextSet.empty
- let a_discharge : Opaqueproof.cooking_info list = []
-
- let local_opaque_table = ref (Array.make 100 a_constr)
- let local_univ_table = ref (Array.make 100 a_univ)
- let local_discharge_table = ref (Array.make 100 a_discharge)
- let local_index = ref 0
-
- module FMap = Map.Make(Future.UUID)
- let f2t = ref FMap.empty
-
- let get_opaque dp i =
-   if DirPath.equal dp (Lib.library_dp ())
-   then (!local_opaque_table).(i)
-   else access_opaque_table dp i
- 
- let join_local_opaque dp i =
-   if DirPath.equal dp (Lib.library_dp ()) then
-    ignore(Future.force (!local_opaque_table).(i))
-
- let join_local_univ dp i =
-   if DirPath.equal dp (Lib.library_dp ()) then
-    ignore(Future.join (!local_univ_table).(i))
-
- let get_univ dp i =
-   if DirPath.equal dp (Lib.library_dp ())
-   then Some (!local_univ_table).(i)
-   else try Some (access_univ_table dp i) with Not_found -> None
-
- let store (d,cu) =
-  let n = !local_index in
-  incr local_index;
-  if Int.equal n (Array.length !local_opaque_table) then begin
-    let t = Array.make (2*n) a_constr in
-    Array.blit !local_opaque_table 0 t 0 n;
-    local_opaque_table := t;
-    let t = Array.make (2*n) a_univ in
-    Array.blit !local_univ_table 0 t 0 n;
-    local_univ_table := t;
-    let t = Array.make (2*n) a_discharge in
-    Array.blit !local_discharge_table 0 t 0 n;
-    local_discharge_table := t
-  end;
-  let c, u = Future.split2 ~greedy:true cu in
-  Future.sink u;
-  Future.sink c;
-  (!local_opaque_table).(n) <- c;
-  (!local_univ_table).(n) <- u;
-  (!local_discharge_table).(n) <- d;
-  f2t := FMap.add (Future.uuid cu) n !f2t;
-  Some (Lib.library_dp (), n)
-
- let dump () =
-   Array.sub !local_opaque_table 0 !local_index,
-   Array.sub !local_univ_table 0 !local_index,
-   Array.sub !local_discharge_table 0 !local_index,
-   FMap.bindings !f2t
-
- let reset () =
-   local_discharge_table := Array.make 100 a_discharge;
-   local_univ_table := Array.make 100 a_univ;
-   local_opaque_table := Array.make 100 a_constr;
-   f2t := FMap.empty;
-   local_index := 0
-
-end
+  try
+    Some (access_table 
+            (fetch_table "universe contexts of opaque proofs")
+            add_univ_table !univ_tables dp i)
+  with Not_found -> None
 
 let () =
-  Opaqueproof.set_indirect_opaque_accessor OpaqueTables.get_opaque;
-  Opaqueproof.set_indirect_univ_accessor OpaqueTables.get_univ;
-  Opaqueproof.set_join_indirect_local_opaque OpaqueTables.join_local_opaque;
-  Opaqueproof.set_join_indirect_local_univ OpaqueTables.join_local_univ
+  Opaqueproof.set_indirect_opaque_accessor access_opaque_table;
+  Opaqueproof.set_indirect_univ_accessor access_univ_table
 
 (************************************************************************)
 (* Internalise libraries *)
@@ -694,8 +622,6 @@ let start_library f =
   check_module_name file;
   check_coq_overwriting ldir0 id;
   let ldir = add_dirpath_suffix ldir0 id in
-  OpaqueTables.reset ();
-  Opaqueproof.set_indirect_creator OpaqueTables.store;
   Declaremods.start_library ldir;
   ldir,longf
 
@@ -743,7 +669,7 @@ let error_recursively_dependent_library dir =
 (* Security weakness: file might have been changed on disk between
    writing the content and computing the checksum... *)
 
-let save_library_to ?todo dir f =
+let save_library_to ?todo dir f otab =
   let f, todo, utab, dtab =
     match todo with
     | None ->
@@ -753,10 +679,8 @@ let save_library_to ?todo dir f =
         assert(!Flags.compilation_mode = Flags.BuildVi);
         f ^ "i", (fun x -> Some (d x)),
           (fun x -> Some (x,Univ.ContextSet.empty,false)), (fun x -> Some x) in
-  Opaqueproof.reset_indirect_creator ();
   let cenv, seg, ast = Declaremods.end_library dir in
-  let opaque_table, univ_table, disch_table, f2t_map =
-    OpaqueTables.dump () in
+  let opaque_table, univ_table, disch_table, f2t_map = Opaqueproof.dump otab in
   assert(!Flags.compilation_mode = Flags.BuildVi ||
          Array.for_all Future.is_val opaque_table);
   let md = {
diff --git a/library/library.mli b/library/library.mli
index 5154c25e4..c92b9d623 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -43,8 +43,8 @@ val import_module : bool -> qualid located -> unit
 val start_library : string -> DirPath.t * string
 
 (** {6 End the compilation of a library and save it to a ".vo" file } *)
-val save_library_to : ?todo:((Future.UUID.t * int) list -> 'tasks) ->
-  DirPath.t -> string -> unit
+val save_library_to : ?todo:(int Future.UUIDMap.t -> 'tasks) ->
+  DirPath.t -> string -> Opaqueproof.opaquetab -> unit
 
 val load_library_todo :
   string -> string * seg_lib * seg_univ * seg_discharge * 'tasks * seg_proofs
diff --git a/library/universes.ml b/library/universes.ml
index cc0153311..708324aed 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -310,7 +310,10 @@ let unsafe_instance_from ctx =
 let fresh_constant_instance env c inst =
   let cb = lookup_constant c env in
     if cb.Declarations.const_polymorphic then
-      let inst, ctx = fresh_instance_from (Declareops.universes_of_constant cb) inst in
+      let inst, ctx =
+        fresh_instance_from
+          (Declareops.universes_of_constant (Environ.opaque_tables env) cb) inst
+      in
 	((c, inst), ctx)
     else ((c,Instance.empty), ContextSet.empty)
 
@@ -331,7 +334,8 @@ let fresh_constructor_instance env (ind,i) inst =
 let unsafe_constant_instance env c =
   let cb = lookup_constant c env in
     if cb.Declarations.const_polymorphic then
-      let inst, ctx = unsafe_instance_from (Declareops.universes_of_constant cb) in
+      let inst, ctx = unsafe_instance_from
+        (Declareops.universes_of_constant (Environ.opaque_tables env) cb) in
 	((c, inst), ctx)
     else ((c,Instance.empty), UContext.empty)
 
@@ -441,7 +445,7 @@ let type_of_reference env r =
      let cb = Environ.lookup_constant c env in
      let ty = Typeops.type_of_constant_type env cb.const_type in
        if cb.const_polymorphic then
-	 let inst, ctx = fresh_instance_from (Declareops.universes_of_constant cb) None in
+	 let inst, ctx = fresh_instance_from (Declareops.universes_of_constant (Environ.opaque_tables env) cb) None in
 	   Vars.subst_instance_constr inst ty, ctx
        else ty, ContextSet.empty
 
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index ea2239673..cae7f0999 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -1013,7 +1013,7 @@ let extract_constant env kn cb =
 	  | OpaqueDef c ->
 	    add_opaque r;
 	    if access_opaque () then
-              mk_typ (Opaqueproof.force_proof c)
+              mk_typ (Opaqueproof.force_proof (Environ.opaque_tables env) c)
             else mk_typ_ax ())
     | (Info,Default) ->
         (match cb.const_body with
@@ -1022,7 +1022,7 @@ let extract_constant env kn cb =
 	  | OpaqueDef c ->
 	    add_opaque r;
 	    if access_opaque () then
-              mk_def (Opaqueproof.force_proof c)
+              mk_def (Opaqueproof.force_proof (Environ.opaque_tables env) c)
             else mk_ax ())
 
 let extract_constant_spec env kn cb =
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index cd3f1a5d4..b740e192a 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -948,8 +948,7 @@ let generate_equation_lemma 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 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 (body_of_constant f_def)
-  in
+  let f_body = Option.get (Global.body_of_constant_body f_def)in
   let params,f_body_with_params = decompose_lam_n nb_params f_body in
   let (_,num),(_,_,bodies) = destFix f_body_with_params in
   let fnames_with_params =
@@ -1065,7 +1064,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
       }
     in
     let get_body const =
-      match body_of_constant (Global.lookup_constant const) with
+      match Global.body_of_constant const with
 	| Some body ->
 	     Tacred.cbv_norm_flags
 	       (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index c4a340880..41f3a5a8b 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -384,7 +384,7 @@ let get_funs_constant mp dp =
   in
   function const ->
     let find_constant_body const =
-      match body_of_constant (Global.lookup_constant const) with
+      match Global.body_of_constant const with
 	| Some body ->
 	    let body = Tacred.cbv_norm_flags
 	      (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index b613a4b13..71ebf4923 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -763,7 +763,7 @@ let make_graph (f_ref:global_reference) =
       | _ -> raise (UserError ("", str "Not a function reference") )
   in
   Dumpglob.pause ();
-  (match body_of_constant c_body with
+  (match Global.body_of_constant_body 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 e0f6ef25c..efdbb0dc4 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -470,10 +470,10 @@ let ungeneralized_type_of_constant_type t =
 
 let print_constant with_values sep sp =
   let cb = Global.lookup_constant sp in
-  let val_0 = Declareops.body_of_constant cb in
+  let val_0 = Global.body_of_constant_body cb in
   let typ = Declareops.type_of_constant cb in
   let typ = ungeneralized_type_of_constant_type typ in
-  let univs = Univ.instantiate_univ_context (Declareops.universes_of_constant cb) in
+  let univs = Univ.instantiate_univ_context (Global.universes_of_constant_body cb) in
   hov 0 (pr_polymorphic cb.const_polymorphic ++
     match val_0 with
     | None ->
@@ -626,7 +626,7 @@ let print_full_pure_context () =
 	      | OpaqueDef lc ->
 		str "Theorem " ++ print_basename con ++ cut () ++
 		str " : " ++ pr_ltype typ ++ str "." ++ fnl () ++
-		str "Proof " ++ pr_lconstr (Opaqueproof.force_proof lc)
+		str "Proof " ++ pr_lconstr (Opaqueproof.force_proof (Global.opaque_tables ()) lc)
 	      | Def c ->
 		str "Definition " ++ print_basename con ++ cut () ++
 		str "  : " ++ pr_ltype typ ++ cut () ++ str " := " ++
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index 36f2b14cb..b0fea5916 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -47,7 +47,7 @@ let retrieve_first_recthm = function
       (pi2 (Global.lookup_named id),variable_opacity id)
   | ConstRef cst ->
       let cb = Global.lookup_constant cst in
-      (body_of_constant cb, is_opaque cb)
+      (Global.body_of_constant_body cb, is_opaque cb)
   | _ -> assert false
 
 let adjust_guardness_conditions const = function
diff --git a/stm/stm.ml b/stm/stm.ml
index 3e8181fe9..b68ef9496 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -805,8 +805,9 @@ module Task = struct
         List.iter (fun (_,se) -> Declareops.iter_side_effects (function
           | Declarations.SEsubproof(_,
              { Declarations.const_body = Declarations.OpaqueDef f;
-      	 const_universes = univs } ) ->
-              Opaqueproof.join_opaque f
+      	       const_universes = univs } ) ->
+              (* They are Direct *)
+              Opaqueproof.join_opaque Opaqueproof.empty_opaquetab f
           | _ -> ())
         se) (fst l);
         l, Unix.gettimeofday () -. wall_clock in
@@ -885,7 +886,8 @@ module Slaves : sig
   val slave_init_stdout : unit -> unit
 
   type tasks
-  val dump : (Future.UUID.t * int) list -> tasks
+  val dump_final : int Future.UUIDMap.t -> tasks
+  val dump_snapshot : int Future.UUIDMap.t -> tasks
   val check_task : string -> tasks -> int -> bool
   val info_tasks : tasks -> (string * float * int) list
   val finish_task :
@@ -953,21 +955,24 @@ end = struct
           Nametab.locate_constant
             (Libnames.qualid_of_ident po.Proof_global.id) in
         let c = Global.lookup_constant con in
-        match c.Declarations.const_body with
-        | Declarations.OpaqueDef lc ->
-            let uc = Option.get (Opaqueproof.get_constraints lc) in
-            let uc =
-              Future.chain
-                ~greedy:true ~pure:true uc Univ.hcons_universe_context_set in
-            let pr = Opaqueproof.get_proof lc in
-            let pr = Future.chain ~greedy:true ~pure:true pr discharge in
-            let pr = Future.chain ~greedy:true ~pure:true 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
-        | _ -> assert false
+        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
+        let pr =
+          Future.from_val (Option.get (Global.body_of_constant_body c)) in
+        let uc =
+          Future.chain
+            ~greedy:true ~pure:true uc Univ.hcons_universe_context_set in
+        let pr = Future.chain ~greedy:true ~pure:true pr discharge in
+        let pr = Future.chain ~greedy:true ~pure:true 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 check_task name l i =
     match check_task_aux "" name l i with
@@ -1031,7 +1036,12 @@ end = struct
   let dump f2t_map =
     let tasks = TaskQueue.dump () in
     prerr_endline (Printf.sprintf "dumping %d tasks\n" (List.length tasks));
-    List.map (function r -> { r with r_uuid = List.assoc r.r_uuid f2t_map })
+    List.map (function r -> { r with r_uuid = Future.UUIDMap.find r.r_uuid f2t_map })
+      (CList.map_filter (Task.request_of_task `Fresh) tasks)
+  let dump_snapshot f2t_map =
+    let tasks = TaskQueue.snapshot () in
+    prerr_endline (Printf.sprintf "dumping %d tasks\n" (List.length tasks));
+    List.map (function r -> { r with r_uuid = Future.UUIDMap.find r.r_uuid f2t_map })
       (CList.map_filter (Task.request_of_task `Fresh) tasks)
 
 end
diff --git a/stm/stm.mli b/stm/stm.mli
index 75aa08e7b..d77c19cfb 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -48,7 +48,8 @@ val stop_worker : string -> unit
 val join : unit -> unit
 (* To save to disk an incomplete document *)
 type tasks
-val dump : (Future.UUID.t * int) list -> tasks
+val dump_final : int Future.UUIDMap.t -> tasks
+val dump_snapshot : int Future.UUIDMap.t -> tasks
 
 val check_task : string -> tasks -> int -> bool
 val info_tasks : tasks -> (string * float * int) list
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 248a6b513..dcce58199 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -321,7 +321,7 @@ let compile verbosely f =
       Stm.join ();
       let wall_clock2 = Unix.gettimeofday () in
       check_pending_proofs ();
-      Library.save_library_to ldir long_f_dot_v;
+      Library.save_library_to ldir long_f_dot_v (Global.opaque_tables ());
       Aux_file.record_in_aux_at Loc.ghost "vo_compile_time"
         (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
       Aux_file.stop_aux_file ();
@@ -333,7 +333,8 @@ let compile verbosely f =
       let _ = load_vernac verbosely long_f_dot_v in
       Stm.finish ();
       check_pending_proofs ();
-      Library.save_library_to ~todo:Stm.dump ldir long_f_dot_v
+      Library.save_library_to ~todo:Stm.dump_final ldir long_f_dot_v
+        (Global.opaque_tables ())
   | Vi2Vo ->
       let open Filename in
       let open Library in