The tactic [admit] exits with the "unsafe" status.

It is highlighted in yellow in Coqide.
The unsafe status is tracked throughout the execution of tactics such that
nested calls to admit are caught.

Many function (mainly those building constr with tactics such as typeclass
related stuff, and Function, and a few other like eauto's use of Hint Extern)
drop the unsafe status. This is unfortunate, but a lot of refactoring would
be in order.
Clean up a warning.
Removes Refine from the dev tools now that the module has been deleted.
Removed spurious try/with in Proofview.Notation.(>>=) and (>>==).

They were a hack to avoid looking where exceptions were raised and not
caught. Hopefully I produce a cleaner stack now, catching errors when
it is needed.
Replaced monads.ml by an essentially equivalent proofview_gen.ml generated by extraction.

The goal was to use Coq's partial evaluation capabilities to do manually some
inlining that Ocaml couldn't do. It may be critical as we are defining higher
order combinators in term of others and no inlining means a lot of
unnecessary, short-lived closures built.

With this modification we get back some (but not all) of the loss of performance introduced by threading the monadic type all over the place.
I still have an estimated 15% longer compilation time for Coq.

Makes use of Set Extraction Conservative Types and Set Extraction File Comment
to maintain the relationship between the functions and their types.

Uses an intermediate layer Proofview_monad between Proofview_gen and
Proofview in order to use a hand-written mli to catch potential errors in the
generated file (it uses Extract Constant a lot).

A bug in the extraction of signatures forces to remove the generated
proofview_gen.mli which does not have the correct types.
Adds a new goal selector "all:".

all:tac applies tac to all the focused subgoals.
New option Default Goal Selector.

Set Default Goal Selector "all" prefixes all tactics with "all:" if no selector
is specified (it is overridden by 1: for instance).
Document "all:" and "Set Default Goal Selector".
Makes the Ltac debugger usable again.

This is just a port of the existing design. Basing the tactics on an IO monad
may allow to simplify things a bit.
Small syntax fix to be compatible with Ocaml 3.11.
Fix behaviour of the refine tactic with respect to evars in types.

It used not to propagate discovered constraints on the evars of the
conclusion of the goal.
Fixes parsing of all: followed by a typechecking/evaluation command.

Exceptions raised during parsing are caught by the parser and result in weird
parsing behaviour. Instead I added a special case in vernac_expr which always
raises an error.
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)
Optimisation of partial application followup.

There is in fact no need of "freeze" in get and current as they have no argument hence are not partially applied.
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.