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

15 files changed, 191 insertions, 120 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;