From c1dab62a4ee116e20c53b442dd91084b47bced9f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 27 May 2019 15:47:46 +0200
Subject: 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.
---
 checker/values.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'checker/values.ml')

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