Fix of r16257 in r16205 for "errors raised by check_evar_instance were
no longer trapped by solve_simple_eqn" was incomplete because
"try ... with E as e | e when f e -> ..." means
"try ... with (E as e | e) when f e -> ..." and not
"try ... with E as e | (e when f e) -> ...".

This was the cause for examples 2615.v and 2670.v failing since March 1.
The need for "as e" should have warned me. Sorry for the mistake.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16420 85f007b7-540e-0410-9357-904b9bb8a0f7
Matching patterns: fixed allow_partial_app which was not working on
unnamed Metas; also added matching an applicative prefix (with
non-meta head) of a term against a pattern, to be used by "Search"
(i.e. SearchHead).

This allows "Search" and "SearchPattern" to behave as in 8.4.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16422 85f007b7-540e-0410-9357-904b9bb8a0f7
Renaming SearchAbout into Search and Search into SearchHead.

I hope I did not forget any place to change.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16423 85f007b7-540e-0410-9357-904b9bb8a0f7