STM: simple refactoring
.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

TODO

safe_typing: export should tag the environment as incomplete, clean up
  the future constraint business.
STM: use sec vars in aux file if no Proof using when building .vi

If a proof has no "Proof using" but we are building a .vi and
the aux file contains such piece of info, we use it to process
the proof asynchronously.
CLEANUP policy for delegatoin
Environ: export API to transitively close a set of section variables
Proof_using: suggest to the user how to decorate "Proof"

This module implements some AI to tell the user how he could
decorate "Proof" with a "using BLA" clause.
record in aux arbitrary command execution time (MAKE OPTIONAL, NAMES CLEANUP)