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.

4 files changed, 13 insertions, 9 deletions

diff --git a/library/global.ml b/library/global.ml
index 827b062725..d5ffae7716 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -132,7 +132,7 @@ let exists_objlabel id = Safe_typing.exists_objlabel id (safe_env ())
 
 let opaque_tables () = Environ.opaque_tables (env ())
 
-let body_of_constant_body env cb =
+let body_of_constant_body access env cb =
   let open Declarations in
   let otab = Environ.opaque_tables env in
   match cb.const_body with
@@ -141,11 +141,11 @@ let body_of_constant_body env cb =
   | 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)
+     Some (Opaqueproof.force_proof access otab o, Declareops.constant_polymorphic_context cb)
 
-let body_of_constant_body ce = body_of_constant_body (env ()) ce
+let body_of_constant_body access ce = body_of_constant_body access (env ()) ce
 
-let body_of_constant cst = body_of_constant_body (lookup_constant cst)
+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 3bc2e84054..039124635e 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -318,9 +318,10 @@ let access_univ_table 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 *)
diff --git a/library/library.mli b/library/library.mli
index d2b0c4f202..2c0673c3b1 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -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