One more fix for rewrite: disallow resolving of the (partial) constraints
happening silently in w_unify and handle this explicitely. Class resolution
filters now can test the existential key. Fixes Ergo contrib.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16571 85f007b7-540e-0410-9357-904b9bb8a0f7
Fixing a Not_found and evar not found anomaly found in ATBR,
related to setoid_rewrite t where t containts evars, to be added
to the goal evars.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16573 85f007b7-540e-0410-9357-904b9bb8a0f7
Changing the type of Ltac values. Now they are toplevel generic
arguments. That way we will be able to define interpretation of
tactics without referring to tactic values.

Quite ad-hoc for now.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16574 85f007b7-540e-0410-9357-904b9bb8a0f7
Added Genarg as generic argument type.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16575 85f007b7-540e-0410-9357-904b9bb8a0f7
Totally replaced ad-hoc tactic values by generic arguments. Now
only tactics results are special tactic values represented by
the non-exported tacvalue type.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16576 85f007b7-540e-0410-9357-904b9bb8a0f7
Moving coercion functions out of Tacinterp.

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