v8.4: updating CHANGES

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16412 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.4: Like in r16346, do not filter local definitions (here in the
type-based second-order unification algorithm).

In type-based second-order unification algorithm, protect local
definitions in instances of evars to wrongly be considered as
potentially flexible.

Altogether, this fixes the anomaly in #3003 (even if some additional
work has to be done to improve the resulting error message, see next
commit).

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