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.

1 files changed, 9 insertions, 1 deletions

diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index a3f151ef86..1cf07e7cc7 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -8,6 +8,14 @@ open Environ
 
 (** {6 Checking constants } *)
 
+let get_proof = ref (fun _ _ -> assert false)
+let set_indirect_accessor f = get_proof := f
+
+let indirect_accessor = {
+  Opaqueproof.access_proof = (fun dp n -> !get_proof dp n);
+  Opaqueproof.access_constraints = (fun _ _ -> assert false);
+}
+
 let check_constant_declaration env kn cb =
   Flags.if_verbose Feedback.msg_notice (str "  checking cst:" ++ Constant.print kn);
   (* Locally set the oracle for further typechecking *)
@@ -33,7 +41,7 @@ let check_constant_declaration env kn cb =
   let body = match cb.const_body with
   | Undef _ | Primitive _ -> None
   | Def c -> Some (Mod_subst.force_constr c)
-  | OpaqueDef o -> Some (Opaqueproof.force_proof otab o)
+  | OpaqueDef o -> Some (Opaqueproof.force_proof indirect_accessor otab o)
   in
   let () =
     match body with