3 files changed, 12 insertions, 11 deletions
diff --git a/checker/check.ml b/checker/check.ml
index cc5ad0af4c..76f40dbac2 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -100,16 +100,7 @@ let access_opaque_table dp i =
   assert (i < Array.length t);
   t.(i)
 
-let access_opaque_univ_table dp i =
-  try
-    let t = LibraryMap.find dp !opaque_univ_tables in
-    assert (i < Array.length t);
-    Some t.(i)
-  with Not_found -> None
-
-let () =
-  Opaqueproof.set_indirect_opaque_accessor access_opaque_table;
-  Opaqueproof.set_indirect_univ_accessor access_opaque_univ_table
+let () = Mod_checking.set_indirect_accessor access_opaque_table
 
 let check_one_lib admit senv (dir,m) =
   let md = m.library_compiled in
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
diff --git a/checker/mod_checking.mli b/checker/mod_checking.mli
index 6cff3e6b8c..dbc81c8507 100644
--- a/checker/mod_checking.mli
+++ b/checker/mod_checking.mli
@@ -8,4 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+val set_indirect_accessor : (Names.DirPath.t -> int -> Constr.t option) -> unit
+
 val check_module : Environ.env -> Names.ModPath.t -> Declarations.module_body -> unit