The configure script now outputs the parameters it was fed with in
config/coq_config.ml
[Coercion]s use [Sortclass], not [Prop] (in docs)

Reported By: J. Ian Johnson
More in CHANGES.
Adding a test for bug #3023.
configure.ml fixed wrt Win32 + byte-only + coqide
Spawn: managed processes

The Spawn and Spawned modules factor the operation of spawning
a process.  Both synchronous and asynchronous channels are supported.
Both threaded and glib like main loop models are supported.  Still,
not all combinations are truly tested not equipped with a decent API:
only async + glib and sync + thread are, since these are the models we
use for coqide<->coqtop and coqtop<->worker respectively.
CoqIDE: ported to spawn
STM: ported to spawn
break > 80 cols line
CoqIDE: command line for extra coqtop "flags"

Like the socket for the OCaml debugger
-schedule-vi-checking ported to spawn
Coercions: avoid imperative data structure
Abstracting away coercion indexes in Classops.
Fixing dependent inversion. Some exceptions were not caught by the tactic
monad.
Adding a smartmap[i] operator to maps.
Using Map.smartmap whenever deemed useful.
Fixing backtrace handling here and there.
STM: tell the user if the master is recomputing states validated by workers

When the worker fails, the master may need to recompute some states
the worker has already validates.  In this case they are colored
accordingly.
STM: worker sends back to master the last valid state

So that the master process does not require to compute it.
Still not all valid states are sent back.
Work around for bug in threads + blocking io streamlined