From 1cdfb1f9270e399a784b346c3f8d6abbc4477552 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 4 Jun 2019 10:35:14 +0200
Subject: Remove the discharge segment from vo files.

Since the introduction of delayed section substitution, the opaque table
was already containing the same information.
---
 toplevel/ccompile.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'toplevel')

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 =
-- 
cgit v1.2.3