Remove the discharge segment from vo files.

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

9 files changed, 33 insertions, 40 deletions

diff --git a/checker/check.ml b/checker/check.ml
index 030b605e3f..903258daef 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -337,7 +337,6 @@ let intern_from_file ~intern_mode (dir, f) =
       let (sd:summary_disk), _, digest = marshal_in_segment f ch in
       let (md:library_disk), _, digest = marshal_in_segment f ch in
       let (opaque_csts:seg_univ option), _, udg = marshal_in_segment f ch in
-      let (discharging:'a option), _, _ = marshal_in_segment f ch in
       let (tasks:'a option), _, _ = marshal_in_segment f ch in
       let (table:seg_proofs option), pos, checksum =
         marshal_or_skip ~intern_mode f ch in
@@ -350,7 +349,7 @@ let intern_from_file ~intern_mode (dir, f) =
       if dir <> sd.md_name then
         user_err ~hdr:"intern_from_file"
           (name_clash_message dir sd.md_name f);
-      if tasks <> None || discharging <> None then
+      if tasks <> None then
         user_err ~hdr:"intern_from_file"
           (str "The file "++str f++str " contains unfinished tasks");
       if opaque_csts <> None then begin
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 02d8ff0672..e18b726111 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -130,21 +130,20 @@ module FMap = Future.UUIDMap
 
 let dump ?(except = Future.UUIDSet.empty) { opaque_val = otab; opaque_len = n; _ } =
   let opaque_table = Array.make n ([], 0, None) in
-  let disch_table = Array.make n [] in
   let f2t_map = ref FMap.empty in
   let iter n (univs, d, cu) =
     let uid = Future.uuid cu in
     let () = f2t_map := FMap.add (Future.uuid cu) n !f2t_map in
-    if Future.is_val cu then
-      let (c, _) = Future.force cu in
-      opaque_table.(n) <- (d, univs, Some c)
-    else if Future.UUIDSet.mem uid except then
-      (* Only monomorphic constraints can be delayed currently *)
-      let () = assert (Int.equal univs 0) in
-      disch_table.(n) <- d
-    else
-      CErrors.anomaly
-        Pp.(str"Proof object "++int n++str" is not checked nor to be checked")
+    let c =
+      if Future.is_val cu then
+        let (c, _) = Future.force cu in
+        Some c
+      else if Future.UUIDSet.mem uid except then None
+      else
+        CErrors.anomaly
+          Pp.(str"Proof object "++int n++str" is not checked nor to be checked")
+    in
+    opaque_table.(n) <- (d, univs, c)
   in
   let () = Int.Map.iter iter otab in
-  opaque_table, disch_table, !f2t_map
+  opaque_table, !f2t_map
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 41f5ebb6b3..6e275649cd 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -66,5 +66,4 @@ val join_opaque : ?except:Future.UUIDSet.t -> opaquetab -> opaque -> unit
 
 val dump : ?except:Future.UUIDSet.t -> opaquetab ->
   (cooking_info list * int * Constr.t option) array *
-  cooking_info list array *
   int Future.UUIDMap.t
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
 
diff --git a/stm/stm.ml b/stm/stm.ml
index ad18245dec..1a525f8c80 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1637,7 +1637,7 @@ and Slaves : sig
   val info_tasks : 'a tasks -> (string * float * int) list
   val finish_task :
     string ->
-    Library.seg_univ -> Library.seg_discharge -> Library.seg_proofs ->
+    Library.seg_univ -> Library.seg_proofs ->
     int tasks -> int -> Library.seg_univ
 
   val cancel_worker : WorkerPool.worker_id -> unit
@@ -1722,7 +1722,7 @@ end = struct (* {{{ *)
                       str (Printexc.to_string e)));
       if drop then `ERROR_ADMITTED else `ERROR
 
-  let finish_task name (cst,_) d p l i =
+  let finish_task name (cst,_) p l i =
     let { Stateid.uuid = bucket }, drop = List.nth l i in
     let bucket_name =
       if bucket < 0 then (assert drop; ", no bucket")
@@ -1747,7 +1747,10 @@ end = struct (* {{{ *)
         (* We only manipulate monomorphic terms here. *)
         let () = assert (Univ.AUContext.is_empty ctx) in
         let pr = Constr.hcons pr in
-        p.(bucket) <- d.(bucket), Univ.AUContext.size ctx, Some pr;
+        let (ci, univs, dummy) = p.(bucket) in
+        let () = assert (Option.is_empty dummy) in
+        let () = assert (Int.equal (Univ.AUContext.size ctx) univs) in
+        p.(bucket) <- ci, univs, Some pr;
         Univ.ContextSet.union cst uc, false
 
   let check_task name l i =
@@ -2743,11 +2746,11 @@ let check_task name (tasks,rcbackup) i =
   with e when CErrors.noncritical e -> VCS.restore vcs; false
 let info_tasks (tasks,_) = Slaves.info_tasks tasks
 
-let finish_tasks name u d p (t,rcbackup as tasks) =
+let finish_tasks name u p (t,rcbackup as tasks) =
   RemoteCounter.restore rcbackup;
   let finish_task u (_,_,i) =
     let vcs = VCS.backup () in
-    let u = State.purify (Slaves.finish_task name u d p t) i in
+    let u = State.purify (Slaves.finish_task name u p t) i in
     VCS.restore vcs;
     u in
   try
diff --git a/stm/stm.mli b/stm/stm.mli
index 5e1e9bf5ad..86e2566539 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -167,7 +167,7 @@ type tasks
 val check_task : string -> tasks -> int -> bool
 val info_tasks : tasks -> (string * float * int) list
 val finish_tasks : string ->
-  Library.seg_univ -> Library.seg_discharge -> Library.seg_proofs ->
+  Library.seg_univ -> Library.seg_proofs ->
     tasks -> Library.seg_univ * Library.seg_proofs
 
 (* Id of the tip of the current branch *)
diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml
index 0f78e0acf6..cf0c8934b0 100644
--- a/stm/vio_checking.ml
+++ b/stm/vio_checking.ml
@@ -12,7 +12,7 @@ open Util
 
 let check_vio (ts,f_in) =
   Dumpglob.noglob ();
-  let _, _, _, _, tasks, _ = Library.load_library_todo f_in in
+  let _, _, _, tasks, _ = Library.load_library_todo f_in in
   Stm.set_compilation_hints f_in;
   List.fold_left (fun acc ids -> Stm.check_task f_in tasks ids && acc) true ts
 
@@ -29,7 +29,7 @@ let schedule_vio_checking j fs =
   if j < 1 then CErrors.user_err Pp.(str "The number of workers must be bigger than 0");
   let jobs = ref [] in
   List.iter (fun long_f_dot_vio ->
-    let _,_,_,_, tasks, _ = Library.load_library_todo long_f_dot_vio in
+    let _,_,_, tasks, _ = Library.load_library_todo long_f_dot_vio in
     Stm.set_compilation_hints long_f_dot_vio;
     let infos = Stm.info_tasks tasks in
     let eta = List.fold_left (fun a (_,t,_) -> a +. t) 0.0 infos in
diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml
index 7748134146..2e25066897 100644
--- a/toplevel/ccompile.ml
+++ b/toplevel/ccompile.ml
@@ -176,9 +176,9 @@ let compile opts copts ~echo ~f_in ~f_out =
       Dumpglob.noglob ();
       let long_f_dot_vio, long_f_dot_vo =
         ensure_exists_with_prefix f_in f_out ".vio" ".vo" in
-      let sum, lib, univs, disch, tasks, proofs =
+      let sum, lib, univs, tasks, proofs =
         Library.load_library_todo long_f_dot_vio in
-      let univs, proofs = Stm.finish_tasks long_f_dot_vo univs disch proofs tasks in
+      let univs, proofs = Stm.finish_tasks long_f_dot_vo univs proofs tasks in
       Library.save_library_raw long_f_dot_vo sum lib univs proofs
 
 let compile opts copts ~echo ~f_in ~f_out =