1 files changed, 18 insertions, 5 deletions

diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index b29a52cc..6398b125 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -13,7 +13,7 @@
  * Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud
  *              91405 Orsay, France *)
 
-(* $Id: SetoidTactics.v 10921 2008-05-12 12:27:25Z msozeau $ *)
+(* $Id: SetoidTactics.v 11282 2008-07-28 11:51:53Z msozeau $ *)
 
 Require Export Coq.Classes.RelationClasses.
 Require Export Coq.Classes.Morphisms.
@@ -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).
 
@@ -38,7 +49,7 @@ Definition default_relation [ DefaultRelation A R ] := R.
 
 (** Every [Equivalence] gives a default relation, if no other is given (lowest priority). *)
 
-Instance equivalence_default [ Equivalence A R ] : DefaultRelation A R | 4.
+Instance equivalence_default [ Equivalence A R ] : DefaultRelation R | 4.
 
 (** The setoid_replace tactics in Ltac, defined in terms of default relations and
    the setoid_rewrite tactic. *)
@@ -174,3 +185,5 @@ Ltac default_add_morphism_tactic :=
   end.
 
 Ltac add_morphism_tactic := default_add_morphism_tactic.
+
+Ltac obligation_tactic ::= program_simpl.