Removing native_name reference from constant_body.

For now, this reference (renamed to link_info) has been moved to the
environment (for constants and inductive types). But this is only a first step
towards making the native compiler more functional.
Revert "Partial revert of r16711"

The sharing introduced by this commit is now correct, since a reference used by
the native compiler has been removed from constant_body.

This reverts commit 413f5fcd4bf581ff3ea4694c193d637589c7d54f.
Got rid of unused lazy flag in the native compiler.
Avoid generating .ml files in native compiler.
Support for evars and metas in native compiler.

Experimental. Turned out to be much harder to implement than I thought. The main
issue is that the reification in the native compiler and the VM is not quite
untyped. Indeed, type annotations for lambdas have to be reconstructed. Hence,
when reifying an application u = t a1 ... an, the type of t has to be known or
reconstructed. It is always possible to do so in plain CIC, when u is in normal
form and its type is known. However, with partial terms this may no longer be
the case, as in: ?1 a1 ... an. So we also compile and evaluate the type of
evars and metas.

This still has to be tested more extensively, but the correction of the kernel
native conversion (on terms without evars or metas) should not be impacted.

Much of this could be reused for the VM.
Useless Evd.create_evar_defs.
When resetting an evarmap with the unsafe function Evd.evars_reset_evd with
the flag with_conv_pbs, only reset the metas, not the last_mod field. It seemed
strange to mix two unrelated things. This did not break anything visible...
Reference the 'external' tactic.
Code cleaning in Rewrite, may also result faster.
Remove obsolete comment about Let being processed synchronously

Let proof terms are stocked in the named_context that is used directly
everywhere, hence there is no way to stock a Future proof term there.
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