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 /checker/check.ml | |
| 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 'checker/check.ml')
| -rw-r--r-- | checker/check.ml | 3 |
1 files changed, 1 insertions, 2 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 |