Remove the discharge segment from vo files.

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

3 files changed, 11 insertions, 8 deletions

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