Prepare the new patch level

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.3@15830 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.3: Removed mention of configure's option -nowarning in INSTALL file.
This option had actually never been released (it only existed for 2
days long in August 1999).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.3@15903 85f007b7-540e-0410-9357-904b9bb8a0f7
Coqmktop: a missing -I (fix #2851)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.3@15925 85f007b7-540e-0410-9357-904b9bb8a0f7
Extraction of projections: restrict a hack to ocaml only (fix #2941)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.3@16076 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.3: Fixed a bug in the algorithm elaborating a "match" return predicate.

This occurred in a second choice strategy which is anyway probably not
used in general, but the bug showed up in error messages since these
messages reports on the second choice when the first choice has failed
because of user-side typing error.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.3@16080 85f007b7-540e-0410-9357-904b9bb8a0f7
Envar: in w32, add .exe when searching for caml binaries

 Based on a patch by Pierre-Yves Strub

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.3@16126 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.3: Fixed bug #2967 (missing check on ill-formed recursive notation strings).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.3@16157 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.3: Fixed bug #2966 (de Bruijn error in computation of heads for coercions).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.3@16170 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.3: Fixed bug #2955 (anomaly when calling simpl on constants from aliased modules).

The cache for simpl was not consistently behaving wrt modules: entries
were compared with canonical name only but how far to unfold was
relying on full kernel name. Adopted indexation on full kernel names
(though the other choice is probably ok too).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.3@16179 85f007b7-540e-0410-9357-904b9bb8a0f7
Fixed #2839 and #2981 (anomaly NotASort in retyping). Was due to
collision between two variables of same name, but finally made a
slightly different implementation of sort_of_atomic_type.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.3@16187 85f007b7-540e-0410-9357-904b9bb8a0f7
Firstorder: record with defined field aren't conjonctions (fix #2629)

 The let-in in the type of constructor was perturbating the
 Hipattern.dependent check, leading firstorder to consider too much
 inductives as dependent-free conjonctions, ending with lift errors
 (UNBOUND_REL_-2, ouch).

 This patch is probably overly cautious : if the variable of the
 let-in is used, we consider the constructor to be dependent.
 If someday somebody feels it necessary, he/she could try to reduce
 the let-in's instead...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.3@16341 85f007b7-540e-0410-9357-904b9bb8a0f7
Avoid Pervasives.(=) on some global_reference (fix #2750)

This is actually a partial backport of trunk commit 15999

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.3@16359 85f007b7-540e-0410-9357-904b9bb8a0f7
Add the test-case of bug 2750 in the test-suite

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.3@16360 85f007b7-540e-0410-9357-904b9bb8a0f7
Avoid using Pervasives.compare for Globrevtab (fix #2734)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.3@16364 85f007b7-540e-0410-9357-904b9bb8a0f7
Typo in refman (fix #2962)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.3@16371 85f007b7-540e-0410-9357-904b9bb8a0f7
Coqc: accept -exclude-dir option (fix #3025)

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

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.3@16553 85f007b7-540e-0410-9357-904b9bb8a0f7
Lablgtk2 was not properly included at linking time by coqmktop because of wrong
parentheses.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.3@16572 85f007b7-540e-0410-9357-904b9bb8a0f7
configure: CAML_LD_LIBRARY_PATH is enriched, not overwritten

 Keeping the earlier content of this variable is crucial for opam
 (at least).

 Thanks to François Bobot and Thomas Refis for this one...
Typo resulting in bad eta-expansion of destructing let's body.