v8.1: Removed mention of configure's option -nowarning in INSTALL file.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.1@15905 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.1@16189 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.1: Typo resulting in bad eta-expansion of match's or destructing let's body.
v8.1: 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).