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/check.ml | |
| 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/check.ml')
| -rw-r--r-- | checker/check.ml | 11 |
1 files changed, 1 insertions, 10 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 |