Remove the indirect opaque accessor hooks from Opaqueproof.

We simply pass them as arguments, now that they are not called by the
kernel anymore.

The checker definitely needs to access the opaque proofs. In order not to
touch the API at all, I added a hook there, but it could also be provided
as an additional argument, at the cost of changing all the upwards callers.

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
-