diff options
| author | Pierre-Marie Pédrot | 2019-05-27 15:47:46 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-27 17:52:51 +0200 |
| commit | c1dab62a4ee116e20c53b442dd91084b47bced9f (patch) | |
| tree | 044d033a75d2f715dabd0b1d6bb7b80dc07fe75a /checker/mod_checking.ml | |
| parent | c371b6f0bc6aa75fb3fe138d2bd52bdd189550b1 (diff) | |
Remove the delayed universe table from object files.
This was virtually dead code. The only place really accessing this data was the
user pretty-printer, but actually the tables were not installed for vanilla vo
files.
In practice, that meant that the only case where an access to this table could
have been triggered would have been to print a term coming from a vio file,
or a vo file generated via vio2vo. In all other cases, the printer would not
have displayed the internal universes. While the latter might be considered
a bug, I am instead convinced that this notion of user-facing internal universes
needs to be handled by another mechanism, the current one making little sense.
The fact it was broken all along without anybody noticing proves my point.
Diffstat (limited to 'checker/mod_checking.ml')
| -rw-r--r-- | checker/mod_checking.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 1cf07e7cc7..1bc5891517 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -13,7 +13,6 @@ 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 = |