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
Vector: missing injection lemmas and better impossible branches

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14999 85f007b7-540e-0410-9357-904b9bb8a0f7
In the syntax of pattern matching, "in" clauses are patterns.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15000 85f007b7-540e-0410-9357-904b9bb8a0f7
In the syntax of pattern matching, the arguments of the inductive in the "in"
clause can be any pattern.

It is expanded as a match in the return clause.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15001 85f007b7-540e-0410-9357-904b9bb8a0f7
RefMan update about match syntax.

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

I love being push under presure to commit and do not try my fixup !

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

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15004 85f007b7-540e-0410-9357-904b9bb8a0f7
correcting a little bug in invfun.ml

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