Using the whole tactic environment while Pretyping.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16605 85f007b7-540e-0410-9357-904b9bb8a0f7
Cleaning up the type of Tacinterp.extract_ltac_constr_values.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16606 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].
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".