Remove the discharge segment from vo files.

Since the introduction of delayed section substitution, the opaque table
was already containing the same information.

2 files changed, 8 insertions, 15 deletions

diff --git a/library/library.ml b/library/library.ml
index 8030b835be..1ac75d2fdc 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -323,7 +323,6 @@ type seg_sum = summary_disk
 type seg_lib = library_disk
 type seg_univ = (* true = vivo, false = vi *)
   Univ.ContextSet.t * bool
-type seg_discharge = Opaqueproof.cooking_info list array
 type seg_proofs = (Opaqueproof.cooking_info list * int * Constr.t option) array
 
 let mk_library sd md digests univs =
@@ -348,7 +347,6 @@ let intern_from_file f =
   let ((lmd : seg_lib delayed), digest_lmd) = in_delayed f ch in
   let (univs : seg_univ option), _, digest_u = System.marshal_in_segment f ch in
   let _ = System.skip_in_segment f ch in
-  let _ = System.skip_in_segment f ch in
   let ((del_opaque : seg_proofs delayed),_) = in_delayed f ch in
   close_in ch;
   register_library_filename lsd.md_name f;
@@ -531,15 +529,13 @@ let load_library_todo f =
   let (s0 : seg_sum), _, _ = System.marshal_in_segment f ch in
   let (s1 : seg_lib), _, _ = System.marshal_in_segment f ch in
   let (s2 : seg_univ option), _, _ = System.marshal_in_segment f ch in
-  let (s3 : seg_discharge option), _, _ = System.marshal_in_segment f ch in
   let tasks, _, _ = System.marshal_in_segment f ch in
-  let (s5 : seg_proofs), _, _ = System.marshal_in_segment f ch in
+  let (s4 : seg_proofs), _, _ = System.marshal_in_segment f ch in
   close_in ch;
   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 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
+  s0, s1, Option.get s2, Option.get tasks, s4
 
 (************************************************************************)
 (*s [save_library dir] ends library [dir] and save it to the disk. *)
@@ -582,10 +578,10 @@ 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, disch_table, f2t_map = Opaqueproof.dump ~except otab in
-  let tasks, utab, dtab =
+  let opaque_table, f2t_map = Opaqueproof.dump ~except otab in
+  let tasks, utab =
     match todo with
-    | None -> None, None, None
+    | None -> None, None
     | Some (tasks, rcbackup) ->
         let tasks =
           List.map Stateid.(fun (r,b) ->
@@ -593,8 +589,8 @@ 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.ContextSet.empty,false),
-        Some disch_table in
+        Some (Univ.ContextSet.empty,false)
+  in
   let sd = {
     md_name = dir;
     md_deps = Array.of_list (current_deps ());
@@ -614,7 +610,6 @@ let save_library_to ?todo ~output_native_objects dir f otab =
     System.marshal_out_segment f' ch (sd           : seg_sum);
     System.marshal_out_segment f' ch (md           : seg_lib);
     System.marshal_out_segment f' ch (utab         : seg_univ option);
-    System.marshal_out_segment f' ch (dtab         : seg_discharge option);
     System.marshal_out_segment f' ch (tasks        : 'tasks option);
     System.marshal_out_segment f' ch (opaque_table : seg_proofs);
     close_out ch;
@@ -634,7 +629,6 @@ let save_library_raw f sum lib univs proofs =
   System.marshal_out_segment f ch (sum        : seg_sum);
   System.marshal_out_segment f ch (lib        : seg_lib);
   System.marshal_out_segment f ch (Some univs : seg_univ option);
-  System.marshal_out_segment f ch (None       : seg_discharge option);
   System.marshal_out_segment f ch (None       : 'tasks option);
   System.marshal_out_segment f ch (proofs     : seg_proofs);
   close_out ch
diff --git a/library/library.mli b/library/library.mli
index 284c66db5b..727eca10cf 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -35,7 +35,6 @@ type seg_sum
 type seg_lib
 type seg_univ = (* all_cst, finished? *)
   Univ.ContextSet.t * bool
-type seg_discharge = Opaqueproof.cooking_info list array
 type seg_proofs = (Opaqueproof.cooking_info list * int * Constr.t option) array
 
 (** Open a module (or a library); if the boolean is true then it's also
@@ -51,7 +50,7 @@ val save_library_to :
 
 val load_library_todo
   :  CUnix.physical_path
-  -> seg_sum * seg_lib * seg_univ * seg_discharge * 'tasks * seg_proofs
+  -> seg_sum * seg_lib * seg_univ * 'tasks * seg_proofs
 
 val save_library_raw : string -> seg_sum -> seg_lib -> seg_univ -> seg_proofs -> unit