Typo in comments.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14972 85f007b7-540e-0410-9357-904b9bb8a0f7
A "Grab Existential Variables" to transform the unresolved evars at the end of a proof into goals.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14973 85f007b7-540e-0410-9357-904b9bb8a0f7
Documentation for Grab Existential Variables.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14974 85f007b7-540e-0410-9357-904b9bb8a0f7
Additional comment on Focus Conditions.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14975 85f007b7-540e-0410-9357-904b9bb8a0f7
Arguments supports extra notation scopes

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14977 85f007b7-540e-0410-9357-904b9bb8a0f7
- Fix dependency computation in eterm to not consider filtered variables.
- Fix handling of evar map in Program coercion code that could forget some new declarations.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14978 85f007b7-540e-0410-9357-904b9bb8a0f7
In [reflexivity], [symmetry] etc, use the type found by looking at the relation as the carrier instead of
the first argument's type (plays nicer with coercions).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14979 85f007b7-540e-0410-9357-904b9bb8a0f7
Fix in evarutil: add a conversion problem for ?x ts = ?x us only if ts and us are not convertible

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14980 85f007b7-540e-0410-9357-904b9bb8a0f7
Avoid unnecessary normalizations w.r.t. evars in Program.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14981 85f007b7-540e-0410-9357-904b9bb8a0f7
Avoid retrying uncessarily to prove independent remaining obligations in Program.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14982 85f007b7-540e-0410-9357-904b9bb8a0f7
Fix handling of space after "Notation" or "where", add missing keywords.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14983 85f007b7-540e-0410-9357-904b9bb8a0f7
Document the [unify] tactic.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14984 85f007b7-540e-0410-9357-904b9bb8a0f7
Correct application of head reduction.
Fix a regression in subtac_pretyping, avoiding application of bidirectional application checking in
case the return type is a subset (bad interaction with typeclass overloading). Should be done only
on constructor applications.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14985 85f007b7-540e-0410-9357-904b9bb8a0f7
- changing minimal version for OCaml: Coq uses Filename.dirsep that is available from OCaml 3.11.2 (see bug #2707)
- fixing outdated address for Coq Club

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14987 85f007b7-540e-0410-9357-904b9bb8a0f7
Use a heuristic to not simplify equality hypotheses remaining after dependent induction if they
don't look really trivial. We still are making a choice though. Fixes bug #2712.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14988 85f007b7-540e-0410-9357-904b9bb8a0f7
Ide: sentences found by find_phrase_starting_at should be nonempty (fix #2683)

 In addition to #2683, this also prevent Vernac.End_of_input
 exceptions when a buffer ends with one of the new delimiters -+*{}.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14989 85f007b7-540e-0410-9357-904b9bb8a0f7
Implement the substitution function for global options. Fixes anomaly in ssreflect compilation

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14991 85f007b7-540e-0410-9357-904b9bb8a0f7
Univ: correct compare_neq (fix #2703)

 The earlier version was a bit too quick to answer <= while strict
 constraints could still appear from remaining universes to explore.
 Typical situation: compare u v when u <= v and u <= w < v.
 Encountering u <= v isn't enough to conclude yet...

 This means that kernels from r13719 to now in trunk, and
 from r13735 to now in 8.3 (including 8.3pl{1,2,3}) couldn't accurately
 detect universe inconsistencies, leading to potential proofs of False!
 Oups, sorry...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14993 85f007b7-540e-0410-9357-904b9bb8a0f7
Coq_makefile: Add of extra options by default

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14997 85f007b7-540e-0410-9357-904b9bb8a0f7
Bug 2703: send stdout dump to coqide when an error occurs.

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