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/values.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/values.ml')
| -rw-r--r-- | checker/values.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/checker/values.ml b/checker/values.ml index 4b651cafb6..2e4b9036d9 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -385,4 +385,4 @@ let v_lib = let v_opaques = Array (Opt v_constr) let v_univopaques = - Opt (Tuple ("univopaques",[|Array (Opt v_context_set);v_context_set;v_bool|])) + Opt (Tuple ("univopaques",[|v_context_set;v_bool|])) |