correcting a little bug in Function

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15947 85f007b7-540e-0410-9357-904b9bb8a0f7
Change [Hints Resolve] to still accept constrs as arguments
to maintain compatibility, the term is then declared as a constant internally.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15948 85f007b7-540e-0410-9357-904b9bb8a0f7
Coqide Detach View: avoid doing gtk stuff in sub-thread (fix #2863)

 In Win32, playing with gtk stuff outside gtk's main loop causes
 coqide to crash: we should be careful when using do_if_not_computing
 and its Thread.create. In the case of Detach View anyway, the
 do_if_not_computing was clearly useless. Strangely, the unix gtk
 seems more resilient and was not crashing ...

 Btw, avoid maintaining a thread-unsafe list of detached_views,
 use instead gtk callbacks to close detached views when their
 corresponding buffer in the main window is closed.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15950 85f007b7-540e-0410-9357-904b9bb8a0f7
Reversed roles of undefined/defined evars in Evd, thus saving precious
time when requesting only undefined evars (which is actually most often
the case, as in Goal.advance). Hopefully this should not disrupt anything.

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