v8.2: 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.2@15904 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.2: Fixed bug #2967 (missing check on ill-formed recursive notation strings).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.2@16158 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.2: 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.2@16171 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.2@16188 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.2: Fixing a typo in the documentation of discriminate.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.2@16554 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.2: Typo resulting in bad eta-expansion of destructing let's body.
v8.2: Fixing bug #3169 and avoiding anomaly in bug #2885 (vm_compute not
supporting metas/evars). Fix of #3169 is by calling pretyping retyper
rather than the non evar-aware kernel type-checker (since argument of
vm_compute is supposed to be already typable).