Optimisation of partial applications in the tactic monad.

Explanations here: https://ocaml.janestreet.com/?q=node/30

Patch by Pierre-Marie Pédrot, with modifications from Arnaud Spiwack.

Signed-off-by: Arnaud Spiwack <arnaud@spiwack.net>
Various rewriting, mostly for speed purposes.

- A variant of tclEVARS directly in the language of the monad
- A variant of tclDISPATCHGEN (tclINDEPENDENT) hopefully faster in the case there is only one tactic to copy
- A better written tclDISPATCHGEN (which may make thing actually a little slower)
- A special case in tclDISPATCHGEN and tclINDEPENDENT for the case when they are 0 or 1 goals (adaptation of a patch sent by Pierre-Marie Pédrot)
Try to remove intermediate allocations when dealing with goal-specific tactics.

Introduces a primitive Goal.enter which allows to access the common information needed by goal-specific tactics, avoids a number of monadic binds, and some unnecessary allocations of lists.
More optimisations of partial applications.

This time in Goal.

Patch by Pierre-Marie Pédrot.

Signed-off-by: Arnaud Spiwack <arnaud@spiwack.net>
Set an extraction flag for inling let-s in Monad.v.

Reduces the size of split significantly. In particular it now uses only 2 matches instead of 4.

Patch by Pierre-Marie Pédrot and Pierre Letouzey.

Signed-off-by: Arnaud Spiwack <arnaud@spiwack.net>
A more principled split.

Instead of interleaving the reifications and reflection steps, split is defined as a series of reification followed by a series of reflection.

The immediate consequence is that split is hoisted out of the Logic interface, and defined in a single block at the end of the file.
State monad implemented in CPS.
bootstrap/Monads.v: A more efficient split.

Exchanges a IO.bind for a Logic.bind. The latter is better inlined.
Typos in a comment.
Added the tactical "tac1 + tac2".

It works pretty much like "tac1 || tac2" except that it has as successes all the successes of tac1 followed by all the successes of tac2 (whereas the latter has either the successes of tac1 (if there is at least one) or those of tac2 (otherwise)).
A better version of Goal.advance.
More Proofview.Goal.enter.

Proofview.Goal.enter is meant to eventually replace the Goal.sensitive monad.

This commit changes the type of Proofview.Goal.enter from taking a four argument function (environment, evar_map, hyps, concl) from a one argument function of abstract type Proofview.Goal.t. It will be both more extensible and more akin to old-style tactics.

This commit also changes the type of Proofview.Goal.{concl,hyps,env} from monadic operations to projection from a Proofview.Goal.t.
Tachmach.New is now in Proofview.Goal.enter style.

As a result the use of the glist-style interface for manipulating goals has almost been removed.
Less use of the list-based interface for goal-bound tactics.
Corrects the semantics of the "+" tactical.

- Treats goals independently
- Honors failure levels
Adds a tactical once.

[once t] does just as [t] but has exactly one success it [t] has at least one success.
A dedicated view type for Proofview_gen.split.

It doesn't seem to affect performances. But the generated code is slightly cleaner.
Refine does beta-reductions.

To avoid the unpleasantness of having beta-redex in terms after an application of refine, refine is followed by lazy beta.
Made Proofview.Goal.hyps a named_context.

There was really no point in having it be a named_context val. The tactics are not going to access the vm cache. Only vm_compute will.
Normalise goals with respect to evars in the new tactics.