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].
A whole new implemenation of the refine tactic.

It now uses the same algorithm as pretyping does.

This produces pretty weird goal when refining pattern matching terms.
Modification of the pattern matching compilation algorithm are pending, hence I will let it be so for now.

The file Zsqrt_compat.v has two temporary [Admitted] related to this issue.
Small change to the IO monad interface: [val ref : 'a -> 'a ref t]

It doesn't matter much, it's simply a matter of aesthetic, so that all functions
in the interface of [Monads.IO] are pure ([IO.run] being the only impure
function but it's not part of the generic interface).
Plug back the declarative mode.

It seems to work ok, but I'm not too confident in the long run.
Cleanup of comments.
The tactic [admit] exists 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.
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.
Monads.v now properly extracts to proofview_gen.ml.

Makes use of Set Extraction Conservative Types and Set Extraction File Comment.

Adds 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 mli
in order to compile Coq.
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.
Fix Show Script.

With "all:" and side effects, more than one goal can be solved at the same time.
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.