From d3c931cd8c84d1b7d9d5763e20221d51700f0709 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 21 May 2019 19:22:30 +0200
Subject: 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.
---
 checker/mod_checking.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'checker/mod_checking.mli')

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
-- 
cgit v1.2.3