Version bump: 8.4pl1

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/tags/V8.4pl1@16115 85f007b7-540e-0410-9357-904b9bb8a0f7
Hashtbl_alt: bug spotted by Enrico

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16120 85f007b7-540e-0410-9357-904b9bb8a0f7
Coqmktop: fix compilation with official camlp4

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

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16123 85f007b7-540e-0410-9357-904b9bb8a0f7
Envar: nicer code to add .exe when searching for caml binaries in win32

 Btw, the previous patch was contributed by Pierr-Yves Strub

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16125 85f007b7-540e-0410-9357-904b9bb8a0f7
Coqide: fix handling of the new StartError exception (fix #2954)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16127 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.4: Slightly improving some debugging printing and error message for modules.

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

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16156 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.4: Fixing one part of #2830 (anomaly "defined twice" due to nested calls to
solve_candidates).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16164 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.4: 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.4@16169 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.4: Fixed synchronicity of filter with evar context in new_goal_with.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16174 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.4: Fixing bug #2969 (admit failing after Grab Existential Variables due
to inconsistency in using evar_hyps which is unfiltered and evar_env
which is filtered).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16176 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.4: 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.4@16178 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.4: Fixed #2970 (made that "remember" eqn name is interpretable as an ltac var).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16182 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.4: Granting bug/wish #2976 (turning anomaly on input_value into nice message)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16183 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.4@16186 85f007b7-540e-0410-9357-904b9bb8a0f7
Fixing bug #2978 (coqide printing debug messages when not in debug mode).

Typical situations concerned by this were when finding word displayed
under pointer for Fn functions.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16190 85f007b7-540e-0410-9357-904b9bb8a0f7
Fixing coqchk compilation after commit r16183 (v8.4 backport)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16192 85f007b7-540e-0410-9357-904b9bb8a0f7
Fix bug 2977

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16193 85f007b7-540e-0410-9357-904b9bb8a0f7
make validate repaired via a temporary fix for #2949

 I simply provide an explicit argument to one of the functors, avoiding
 the faulty use of the "include-to-self" feature there.
 Note that this NZOrderedType functor could also be simply removed
 as in trunk, since it isn't used anywhere.

 Btw, the Not_found in coqchk is now turned into something slightly
 more informative.

 The core of the bug remains: coqtop should check that "include-to-self"
 hasn't produced a chimera (more details in the bug tracker).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16201 85f007b7-540e-0410-9357-904b9bb8a0f7