Getting rid of LtacLocated exception transformer.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16535 85f007b7-540e-0410-9357-904b9bb8a0f7
Fixing warning of deprecated Argument Scopes.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16536 85f007b7-540e-0410-9357-904b9bb8a0f7
Setting "appcontext" as the default behaviour in Ltac matching.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16537 85f007b7-540e-0410-9357-904b9bb8a0f7
More clever implemenation for IStream.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16538 85f007b7-540e-0410-9357-904b9bb8a0f7
Documenting the "appcontext" by default.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16539 85f007b7-540e-0410-9357-904b9bb8a0f7
Make ist (interp_sign) available to TACTIC EXTEND code

In order to do so I had to move the data base of tactics to
tacinterp (from tacintern).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16540 85f007b7-540e-0410-9357-904b9bb8a0f7
newring.ml4: interp constr arg at interp time (not parse time)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16541 85f007b7-540e-0410-9357-904b9bb8a0f7
bwaa, a Pervasive.compare

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16542 85f007b7-540e-0410-9357-904b9bb8a0f7
comments in mli

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16543 85f007b7-540e-0410-9357-904b9bb8a0f7
Why not going inside fixpoint definition with appcontext ?

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16544 85f007b7-540e-0410-9357-904b9bb8a0f7
export Unification.abstract_list_all_with_dependencies

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16545 85f007b7-540e-0410-9357-904b9bb8a0f7
Do not compute fallback eagerly in Evarconv

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16546 85f007b7-540e-0410-9357-904b9bb8a0f7
Removing a useless location in ltac trace mechanism.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16547 85f007b7-540e-0410-9357-904b9bb8a0f7
Modest protection against "injection" and co raising anomaly in
-nois mode.  This is not perfect yet. E.g. "injection" used while
before eq is defined while compiling Logic.v would raise an anomaly.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16548 85f007b7-540e-0410-9357-904b9bb8a0f7
Fixing buggy backtracking in "intros * pat" with failing "pat".

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16549 85f007b7-540e-0410-9357-904b9bb8a0f7
Now interpreting introduction patterns [x1 .. xn] and (x1,..,xn) as an
"injection" tactic when applied on an equality statement. Moreover,
hypotheses are now entered in the left-to-right order.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16550 85f007b7-540e-0410-9357-904b9bb8a0f7
Fixing a typo in the documentation of discriminate.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16551 85f007b7-540e-0410-9357-904b9bb8a0f7
Flags V8_4 for compatibility infrastructure.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16555 85f007b7-540e-0410-9357-904b9bb8a0f7
Making the behavior of "injection ... as ..." more natural:
- hypotheses are introduced in the left-to-right order
- intropatterns have to match the number of generated hypotheses, and,
  if less, new introduction names are automatically generated
- clearing the hypothesis on which injection is applied, if any.

However, this is a source of incompatibilities (for a variant of
injection that is hopefully not used a lot). Compatibility can be
restored by "Unset Injection L2R Pattern Order".

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16556 85f007b7-540e-0410-9357-904b9bb8a0f7
A constructive proof of Fan theorem where paths are represented by predicates.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16557 85f007b7-540e-0410-9357-904b9bb8a0f7