Aux_file: cache information at compile time for later (re)use

For a file dir/a.v the corresponding aux file dir/.a.aux can store
arbitrary data.  It maps a "Loc.t * string" (key) to a "string" (value).

Pretty much anything can fit in this schema, but ATM I see only the
following possible uses:

1) record inferred data, like the set of section variable used, so that
   one can later use this info to process proofs asynchronously (i.e.
   compute their discharged type without knowing the proof term).
2) record timings (how long it takes to build a proof term or check it),
   so that one can take smarter scheduling decisions
3) record a bloated proof trace for automatic tactics, so that one can
   replay it faster (a sort of cache).  For that to be useful an Ltac
   API is required.

The .aux file contains the path of the .v and its md5 hash.  When loaded
it defaults to the empty map is the file is not there or if the .v file
changed.

Not finding some data in the .aux file cannot be a failure, but finding
it may help in many ways.

The current file format is very simple but human readable.  It is
generated/parsed using printf/scanf and in particular the %S formatter
for the value string.  The file format is private to the Aux_file
module: only an abstract interface is provided.

The current file format is not robust in face of local changes.
Any change invalidates the md5 hash (and the Loc.t is very likely to
change too).
STM: record in aux file proof build and check time
STM: set loc for aux file when interpreting vernac
kernel: save in aux the list of section variables used

This has nothing to do with the kernel itself, but it is
the place where this piece of data is inferred.
Future: allow custom action when a delegated future is forced

The default action is to raise NotReady, but one may want to
make the action "blocking" but successful.  Using this device
all delayed proofs can be "delegated".  If there are slaves, they
will eventually pick up the task.  If there are no slaves, then
the future can behave like a regular, non delegated, lazy computation.
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
 coqchk: rejects .vi files
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.
Proof_global: Simpler API for proof_terminator
Lemmas: export standard proof terminator
coqtop: -check-vi-tasks and -schedule-vi-checking

The command `coqtop -check-vi-tasks 1,4,2 a` checks tasks 1 4 2,
in this precise order, stored in a.vi.

The command `coqtop -schedule-vi-checking 4 a b c` reads {a,b,c}.vi
and .{a,b,c}.aux and spits 4 command lines to check all the tasks in
{a,b,c}.vi trying to equally partition the job between the 4 workers,
that can indeed be run in parallel.
The aux file contains the time that it took to check the proofs stored
in the .vi files last time the file was fully checked.

This user interface is still very rough, it should probably run the
workers instead of just printing their command line.
Fix some warnings with ocamlc 4.01
Paral-ITP: cleanup of command line flags and more conservative default

-async-proofs off
  the system behaves as in 8.4
-async-proofs lazy
  proofs are delayed (when possible) but never processed in parallel
-async-proofs on
  proofs are processed in parallel (when possible).  The number of
  workers is 1, can be changed with -async-proofs-j.  Extra options to
  the worker process can be given with -async-proofs-worker-flags.

The default for batch compilation used to be "lazy", now it is "off".
The "lazy" default was there to test the machinery, but it makes very
little sense in a batch scenario.  If you process things sequentially,
you'd better do them immediately instead of accumulating everything in
memory until the end of the file and only then force all lazy computations.

The default for -ideslave was and still is "on".  It becomes dynamically
"lazy" on a per task (proof) basis if the worker dies badly.

Note that by passing "-async-proofs on" to coqc one can produce a .vo
exploiting multiple workers.  But this is rarely profitable given
that master-to-worker communication is inefficient (i.e. it really
depends on the size of proofs v.s. size of system state).
STM: fix error messages while in batch mode (closes: 3196)
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)