STM: take a shallow snapshot for the first proof step

this way it can be directly sent to a slave with no further manipulation

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16836 85f007b7-540e-0410-9357-904b9bb8a0f7
STM: delegate proofs to slaves only if they are not trivial

Still too simple and not configurable

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16837 85f007b7-540e-0410-9357-904b9bb8a0f7
STM: avoid "kill 9 pid" if we know the slave died

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16838 85f007b7-540e-0410-9357-904b9bb8a0f7
STM: number of slaves passed by the command line

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16839 85f007b7-540e-0410-9357-904b9bb8a0f7
Regression test suite for STM

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16840 85f007b7-540e-0410-9357-904b9bb8a0f7
STM: add options to disable fallbacks to ease regression testing

STM falls back to local, lazy, evaluation if the slave dies badly or
if there is a marshalling error.  Both things should never occur, but
is nice to have the system recover if a bug pops up.
Nevertheless during regression testing these fallbacks should be
disabled not to hide a new bug.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16841 85f007b7-540e-0410-9357-904b9bb8a0f7
CoqIDE: when jumping to an error also move the cursor

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16842 85f007b7-540e-0410-9357-904b9bb8a0f7
STM: if -coq-slaves off really imitate the old CoqIDE

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16843 85f007b7-540e-0410-9357-904b9bb8a0f7
STM: understand -coq-slaves-opts extra-env=VAR=val

In this way one can set an env variable for the slave, like the
socket used by ocamldebug to talk remotely to a process

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16844 85f007b7-540e-0410-9357-904b9bb8a0f7
A shallow copy of a pre_env does not contain the vm cache

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16845 85f007b7-540e-0410-9357-904b9bb8a0f7
Fix comment for new string syntax (OCaml trunk).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16846 85f007b7-540e-0410-9357-904b9bb8a0f7
Splitting Class_tactics between code and CAMLP4/5 declarations.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16847 85f007b7-540e-0410-9357-904b9bb8a0f7
Fixing potential evar leak in Equality.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16848 85f007b7-540e-0410-9357-904b9bb8a0f7
Fixing potential evar leak in Rewrite, and removing dead code.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16849 85f007b7-540e-0410-9357-904b9bb8a0f7
Makes the new Proofview.tactic the basic type of Ltac.

On the compilation of Coq, we can see an increase of ~20% compile time on
my completely non-scientific tests. Hopefully this can be fixed.

There are a lot of low hanging fruits, but this is an iso-functionality commit.
With a few exceptions which were not necessary for the compilation of the theories:
- The declarative mode is not yet ported
- The timeout tactical is currently deactivated because it needs some subtle
I/O. The framework is ready to handle it, but I haven't done it yet.
-  For much the same reason, the ltac debugger is unplugged. It will be more
difficult, but will eventually be back.

A few comments:
I occasionnally used a coercion from [unit Proofview.tactic] to the old
[Prooftype.tactic]. It should work smoothely, but loses any backtracking
information: the coerced tactics has at most one success.
- It is used in autorewrite (it shouldn't be a problem there). Autorewrite's
code is fairly old and tricky
- It is used in eauto, mostly for "Hint Extern". It may be an issue as time goes
as we might want to have various success in a "Hint Extern". But it would
require a heavy port of eauto.ml4
- It is used in typeclass eauto, but with a little help from Matthieu, it should
be easy to port the whole thing to the new tactic engine, actually simplifying
the code.
- It is used in fourier. I believe it to be inocuous.
- It is used in firstorder and congruence. I think it's ok. Their code is
somewhat intricate and I'm not sure they would be easy to actually port.
- It is used heavily in Function. And honestly, I have no idea whether it can do
harm or not.

Updates:
(11 June 2013) Pierre-Marie Pédrot contributed the rebase over his new stream based
architecture for Ltac matching (r16533), which avoid painfully and expensively
working around the exception-throwing control flow of the previous API.
Uses Proofview.tclEXTEND more sparingly.

It is used where failures can be caughts (tclORELSE, tclTRY, …) rather than
at each tclTHEN. Hopefully avoiding making things a bit less slow.
Getting rid of Goal.here, and all the related exceptions and combinators.

It was a bad idea. The new API based on lists seems more sensible.
Bases tactics on an IO monad.

It allowed to restore the timeout tactics. It also prepares for the debugging
mechanism to be restored.

['a IO.t] is just [unit -> 'a].
Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations.
A newly introduced variable inside a named context is no longer α-renamed.

Instead, in case of collision, the older name is substituted for a fresh one.
It should also be made inaccessible from the user, but I'll leave this for later.

The goal is to guarantee that [refine (fun x => _)] introduces a binder named [x].