Calling setoid_rewrite on a term H whose type (eq x y) was not an application

of a setoid equality was erroneously considered an assertion failure instead
of an user error.

Note: in this case the tactic should try the rewrite tactic. However, since
rewrite recursively calls setoid_rewrite in this case, this solution can
diverge. This will be fixed in a future commit.


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

0 files changed, 0 insertions, 0 deletions