Tweaking arity & allocation of some basic functions.
Slightly more efficient zip function in Closure.
Hardening the reading function of vo files.
Updating new ftp link to old archives.
Adding fold_left / fold_right function to maps.
Better implementation of summary unfreezing.
Typo resulting in bad eta-expansion of destructing let's body.
Revealed by message on coq-club on 24/11/2013.
Tacinterp: fewer use of old-style goals.

There are many functions in Tacinterp which use a goal as a proxy for the pair of an environment and an evar_map. But do not build LCF tactics with them. They don't play well with the new style of tactics.

I've changed some of them to explicitely take an environment and an evar_map instead.
Factoring: is_section_variable.

In 0c7a77, I inadvertantly re-defined an is_section_variable function.
Remove the Hiddentac module.

Since the new proof engine, Hiddentac has been essentially trivial.
Here is what happened to the functions defined there
- Aliases, or tactics that were trivial to inline were systematically inlined
- Tactics used only in tacinterp have been moved to tacinterp
- Other tactics have been moved to a new module Tactics.Simple.
Do not use ugly Dyn features in the Quote plugin. Use instead the
provided tactic environment to handle open terms.
Adding a generic Int.Map using persistent arrays.
CoqIDE: show error message for parsing errors
STM: restart slave after every proof

The code now passes a cleanup function that, if slave is not
killed, could be used to do some cleanup between two jobs.

ATM I don't know how to reuse the worker without having it
grow in space indefinitely.  Running Gc.compact is too expensive.
Reduction: every n iterations a slaves process checks for interruption

I chose n to be 10000 iterations.  It might be big, but a slave, to check
for a termination request, has to pass the ball to the thread that
sends "regularly" Ticks to the master process.  Thread.yield is a
system call, so we have to do it very rarely.
Use my real email address in .mailmap
First stab at retrocompatible INTERP message
New option --help-XML-protocol to document the XML procol used by -ideslave

Serialize.ml spits out its own documentation.  Not everything is
statically checked, so it risks to get outdated.  Ideas on how
to statically/dynamically check that the doc is in sync are welcome.
Old message Interp returns the state id so that one can BackTo it
Adding generic solvers to term holes. For now, no resolution mechanism nor
parsing is plugged.