Revised the Ltac trace mechanism so that trace breaking due to
interleaving of ltac and ml code is not visible (this particularly
applies to ltac notation ring, which calls ml-level ring_lookup and
Ring again at the ltac level, resulting in non-localisation of "ring"
errors).

Added also missing LtacLocated checks in Class_instance and Proofview.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16204 85f007b7-540e-0410-9357-904b9bb8a0f7
Added propagation of evars unification failure reasons for better
error messages. The architecture of unification error handling
changed, not helped by ocaml for checking that every exceptions is
correctly caught. Report or fix if you find a regression.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16205 85f007b7-540e-0410-9357-904b9bb8a0f7
Locating errors from consider_remaining_unif_problems if possible
(useful when consider_remaining_unif_problems not called via
pretyping.ml, as e.g. from command.ml).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16206 85f007b7-540e-0410-9357-904b9bb8a0f7
A more informative message when the elimination predicate for
destruct, rewrite, etc. is not well-typed.

Also added support for a more informative message when the elimination
predicate is not well-formed while using the smart "second-order"
unification algorithm. However the "abstract_list_all" algorithm seems
to remain more informative though, so we still use this algorithm for
reporting about ill-typed predicates.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16207 85f007b7-540e-0410-9357-904b9bb8a0f7
Displaying environment and unfolding aliases in "cannot_unify"
error. Maybe displaying environment is making output overly verbose,
but this can also be considered an IDE issue, which would e.g. provide
a button to hide/display environment of the error message...

Also added some "make_all_name_different" which should probably
prevent some anomalies "index to an anonymous variable" at error
reporting time.

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