diff options
| author | Pierre-Marie Pédrot | 2019-06-04 10:35:14 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-06-04 11:16:17 +0200 |
| commit | 1cdfb1f9270e399a784b346c3f8d6abbc4477552 (patch) | |
| tree | f11a76b43b4ea825287d22ae15e8d0fe50968d50 /stm/stm.mli | |
| parent | 0f54a91eac98baf076d8be8f52bccdb1de17ea46 (diff) | |
Remove the discharge segment from vo files.
Since the introduction of delayed section substitution, the opaque table
was already containing the same information.
Diffstat (limited to 'stm/stm.mli')
| -rw-r--r-- | stm/stm.mli | 2 |
1 files changed, 1 insertions, 1 deletions
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 *) |