3 files changed, 16 insertions, 5 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).
 
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index e1f04e45a..4d1054553 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -216,7 +216,7 @@ Qed.
 Add Morphism Z.compare with signature Z.eq ==> Z.eq ==> (@eq comparison) as compare_wd.
 Proof. 
 intros x x' Hx y y' Hy.
-rewrite 2 spec_compare_alt; rewrite Hx, Hy; intuition.
+rewrite 2 spec_compare_alt; unfold Z.eq in *; rewrite Hx, Hy; intuition.
 Qed.
 
 Add Morphism Z.lt with signature Z.eq ==> Z.eq ==> iff as NZlt_wd.
diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
index 4f558e80a..d5cb2882c 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
@@ -223,7 +223,7 @@ Qed.
 Add Morphism N.compare with signature N.eq ==> N.eq ==> (@eq comparison) as compare_wd.
 Proof. 
 intros x x' Hx y y' Hy.
-rewrite 2 spec_compare_alt; rewrite Hx, Hy; intuition.
+rewrite 2 spec_compare_alt. unfold N.eq in *. rewrite Hx, Hy; intuition.
 Qed.
 
 Add Morphism N.lt with signature N.eq ==> N.eq ==> iff as NZlt_wd.