2 files changed, 21 insertions, 34 deletions

diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 9f148ee248..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,23 +41,9 @@ 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 not_here () =
   CErrors.user_err Pp.(str "Cannot access opaque delayed proof")
 
-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 create cu = Direct ([],cu)
 
 let turn_indirect dp o tab = match o with
@@ -97,26 +88,26 @@ 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 match !get_opaque dp i with
+        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 -> u
 
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 3b61ec71ef..4646206e55 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -35,10 +35,19 @@ 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
+    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
@@ -64,16 +73,3 @@ val dump : ?except:Future.UUIDSet.t -> opaquetab ->
   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 option) -> unit
-val set_indirect_univ_accessor :
-  (DirPath.t -> int -> Univ.ContextSet.t option) -> unit
-