Changement de comportement de rewrite: face a une egalité setoid, on

arrete de reduire brutalement pour essayer de tomber sur une egalité
Coq. Au contraire, si la relation de tete est une relation declarée 
dans la base des setoids, on l'utilise. 

ATTENTION: ceci brise la compatibilité, dans le cas très improbable 
ou quelqu'un aurait defini un setoid mais exploiterait la "feature" 
de la reduction vers l'eventuelle egalité Coq sous-jacente. 



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

0 files changed, 0 insertions, 0 deletions