.vi files: .vo files without proofs

File format:
 The .vo file format changed:
   - after the magic number there are 3 segments. A segment is made of 3
     components: bynary int, an ocaml value, a digest.  The binary int
     is the position of the digest, so that one can skip the value without
     unmarshalling it
   - the first segment is the library, as before
   - the second segment is the STM task list
   - the third segment is the opaque table, as before
 A .vo file has a complete opaque table (all proof terms are there).
 A .vi file follows the same format of a .vo file, but some entries
 in the opaque table are missing.  A proof task is stocked instead.

Utilities:
 coqc: option -quick generates a .vi insted of a .vo
 coq_makefile: target quick to generate all .vi
 coqdep: generate deps for .vi files too
 votour: can browse .vi files too, the first question is which segment
         should be read
 coqchk: rejects .vi files

1 files changed, 4 insertions, 0 deletions

diff --git a/lib/system.mli b/lib/system.mli
index 2513ca19d..2e286a40c 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -52,6 +52,10 @@ val marshal_in : string -> in_channel -> 'a
 val digest_out : out_channel -> Digest.t -> unit
 val digest_in : string -> in_channel -> Digest.t
 
+val marshal_out_segment : string -> out_channel -> 'a -> unit
+val marshal_in_segment : string -> in_channel -> 'a * int * Digest.t
+val skip_in_segment : string -> in_channel -> int * Digest.t
+
 (** {6 Sending/receiving once with external executable } *)
 
 val connect : (out_channel -> unit) -> (in_channel -> 'a) -> string -> 'a