Even better test for choosing rewrite or setoid_rewrite.

Now there is a class "SetoidRelation" for registering relations that
should always be considered as setoids and never unfolded. Every "Add
Relation" command adds an instance and impl,iff are there by
default. Now the test is: if there is a SetoidRelation instance, use it
; otherwise, allow unfolding to find an eq or fallback on
setoid_rewrite. To avoid searching for SetoidRelation instances
repeateadly we check that it is really needed first by unfolding the
hyp. Only two scripts relied on the now-forbidden semantics of rewriting
by an @eq inside a setoid relation, in Numbers.


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

1 files changed, 14 insertions, 3 deletions

diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index e939d3ee7..f8b7f62e9 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -24,11 +24,22 @@ Require Export Coq.Relations.Relation_Definitions.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
+(** Setoid relation on a given support: declares a relation as a setoid
+   for use with rewrite. It helps choosing if a rewrite should be handled
+   by setoid_rewrite or the regular rewrite using leibniz equality.
+   Users can declare an [SetoidRelation A RA] anywhere to declare default 
+   relations. This is also done automatically by the [Declare Relation A RA]
+   commands. *)
+
+Class SetoidRelation A (R : relation A).
+
+Instance impl_setoid_relation : SetoidRelation impl.
+Instance iff_setoid_relation : SetoidRelation iff.
+
 (** Default relation on a given support. Can be used by tactics
    to find a sensible default relation on any carrier. Users can 
-   declare an [Instance A RA] anywhere to declare default relations.
-   This is also done by the [Declare Relation A RA] command with no
-   parameters for backward compatibility. *)
+   declare an [Instance def : DefaultRelation A RA] anywhere to 
+   declare default relations. *)
 
 Class DefaultRelation A (R : relation A).