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.
---
 library/library.ml  | 25 ++++++-------------------
 library/library.mli |  4 ++--
 2 files changed, 8 insertions(+), 21 deletions(-)

(limited to 'library')

diff --git a/library/library.ml b/library/library.ml
index 039124635e..e3b8511af1 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -281,13 +281,9 @@ type 'a table_status =
 
 let opaque_tables =
   ref (LibraryMap.empty : (Constr.constr table_status) LibraryMap.t)
-let univ_tables =
-  ref (LibraryMap.empty : (Univ.ContextSet.t table_status) LibraryMap.t)
 
 let add_opaque_table dp st =
   opaque_tables := LibraryMap.add dp st !opaque_tables
-let add_univ_table dp st =
-  univ_tables := LibraryMap.add dp st !univ_tables
 
 let access_table what tables dp i =
   let t = match LibraryMap.find dp !tables with
@@ -312,15 +308,8 @@ let access_opaque_table dp i =
   let what = "opaque proofs" in
   access_table what opaque_tables dp i
 
-let access_univ_table dp i =
-  try
-    let what = "universe contexts of opaque proofs" in
-    access_table what univ_tables dp i
-  with Not_found -> None
-
 let indirect_accessor = {
   Opaqueproof.access_proof = access_opaque_table;
-  Opaqueproof.access_constraints = access_univ_table;
 }
 
 (************************************************************************)
@@ -329,7 +318,7 @@ let indirect_accessor = {
 type seg_sum = summary_disk
 type seg_lib = library_disk
 type seg_univ = (* true = vivo, false = vi *)
-  Univ.ContextSet.t option array * Univ.ContextSet.t * bool
+  Univ.ContextSet.t * bool
 type seg_discharge = Opaqueproof.cooking_info list array
 type seg_proofs = Constr.constr option array
 
@@ -363,11 +352,9 @@ let intern_from_file f =
   let open Safe_typing in
   match univs with
   | None -> mk_library lsd lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty
-  | Some (utab,uall,true) ->
-      add_univ_table lsd.md_name (Fetched utab);
+  | Some (uall,true) ->
       mk_library lsd lmd (Dvivo (digest_lmd,digest_u)) uall
-  | Some (utab,_,false) ->
-      add_univ_table lsd.md_name (Fetched utab);
+  | Some (_,false) ->
       mk_library lsd lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty
 
 module DPMap = Map.Make(DirPath)
@@ -547,7 +534,7 @@ let load_library_todo f =
   if tasks = None then user_err ~hdr:"restart" (str"not a .vio file");
   if s2 = None then user_err ~hdr:"restart" (str"not a .vio file");
   if s3 = None then user_err ~hdr:"restart" (str"not a .vio file");
-  if pi3 (Option.get s2) then user_err ~hdr:"restart" (str"not a .vio file");
+  if snd (Option.get s2) then user_err ~hdr:"restart" (str"not a .vio file");
   s0, s1, Option.get s2, Option.get s3, Option.get tasks, s5
 
 (************************************************************************)
@@ -591,7 +578,7 @@ let save_library_to ?todo ~output_native_objects dir f otab =
         List.fold_left (fun e (r,_) -> Future.UUIDSet.add r.Stateid.uuid e)
           Future.UUIDSet.empty l in
   let cenv, seg, ast = Declaremods.end_library ~output_native_objects ~except dir in
-  let opaque_table, univ_table, disch_table, f2t_map = Opaqueproof.dump ~except otab in
+  let opaque_table, disch_table, f2t_map = Opaqueproof.dump ~except otab in
   let tasks, utab, dtab =
     match todo with
     | None -> None, None, None
@@ -602,7 +589,7 @@ let save_library_to ?todo ~output_native_objects dir f otab =
             with Not_found -> assert b; { r with uuid = -1 }, b)
           tasks in
         Some (tasks,rcbackup),
-        Some (univ_table,Univ.ContextSet.empty,false),
+        Some (Univ.ContextSet.empty,false),
         Some disch_table in
   let sd = {
     md_name = dir;
diff --git a/library/library.mli b/library/library.mli
index 2c0673c3b1..142206e2c5 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -33,8 +33,8 @@ val require_library_from_dirpath
 (** Segments of a library *)
 type seg_sum
 type seg_lib
-type seg_univ = (* cst, all_cst, finished? *)
-  Univ.ContextSet.t option array * Univ.ContextSet.t * bool
+type seg_univ = (* all_cst, finished? *)
+  Univ.ContextSet.t * bool
 type seg_discharge = Opaqueproof.cooking_info list array
 type seg_proofs = Constr.constr option array
 
-- 
cgit v1.2.3