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.
---
 stm/stm.ml | 13 ++++++-------
 1 file changed, 6 insertions(+), 7 deletions(-)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index e32b6c9f1c..21f5ece244 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1819,15 +1819,15 @@ end = struct (* {{{ *)
                       str (Printexc.to_string e)));
       if drop then `ERROR_ADMITTED else `ERROR
 
-  let finish_task name (u,cst,_) d p l i =
+  let finish_task name (cst,_) d p l i =
     let { Stateid.uuid = bucket }, drop = List.nth l i in
     let bucket_name =
       if bucket < 0 then (assert drop; ", no bucket")
       else Printf.sprintf ", bucket %d" bucket in
     match check_task_aux bucket_name name l i with
     | `ERROR -> exit 1
-    | `ERROR_ADMITTED -> u, cst, false
-    | `OK_ADMITTED -> u, cst, false
+    | `ERROR_ADMITTED -> cst, false
+    | `OK_ADMITTED -> cst, false
     | `OK (po,_) ->
         let discharge c = List.fold_right Cooking.cook_constr d.(bucket) c in
         let con =
@@ -1846,9 +1846,8 @@ end = struct (* {{{ *)
         let pr = map (Option.get (Global.body_of_constant_body Library.indirect_accessor c)) in
         let pr = discharge pr in
         let pr = Constr.hcons pr in
-        u.(bucket) <- Some uc;
         p.(bucket) <- Some pr;
-        u, Univ.ContextSet.union cst uc, false
+        Univ.ContextSet.union cst uc, false
 
   let check_task name l i =
     match check_task_aux "" name l i with
@@ -2851,8 +2850,8 @@ let finish_tasks name u d p (t,rcbackup as tasks) =
     VCS.restore vcs;
     u in
   try
-    let u, a, _ = List.fold_left finish_task u (info_tasks tasks) in
-    (u,a,true), p
+    let a, _ = List.fold_left finish_task u (info_tasks tasks) in
+    (a,true), p
   with e ->
     let e = CErrors.push e in
     msg_warning (str"File " ++ str name ++ str ":" ++ spc () ++ iprint e);
-- 
cgit v1.2.3