diff options
| author | Pierre-Marie Pédrot | 2019-05-21 19:22:30 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-24 09:00:10 +0200 |
| commit | d3c931cd8c84d1b7d9d5763e20221d51700f0709 (patch) | |
| tree | 58ca99c4f6007bc66294c41354bb68bf9d71044b /checker/mod_checking.mli | |
| parent | 2fa3dc389a58ca4a390b99995d82e6c089add163 (diff) | |
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.
Diffstat (limited to 'checker/mod_checking.mli')
| -rw-r--r-- | checker/mod_checking.mli | 2 |
1 files changed, 2 insertions, 0 deletions
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 |