Compatibility fixes, backtrack on definitions of reflexive,

symmetric... classes for now, merging Relations with RelationClasses
requires some non-trivial changes on implicits but also some definitions
are different (e.g. antisymmetric in Classes is defined w.r.t an
equivalence relation and not eq). Move back to Reflexive and so on.
reflexivity-like tactics fail in the same way as before if Setoid was
not imported. There is now a scope for morphism signatures, hence "==>",
"++>" and "-->" can be given different interpretations.


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

8 files changed, 114 insertions, 96 deletions

diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index dd9cfbca5..58aef9a7b 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -19,13 +19,15 @@ Require Export Coq.Program.Basics.
 Require Import Coq.Program.Tactics.
 
 Require Import Coq.Classes.Init.
-Require Export Coq.Classes.RelationClasses.
+Require Import Relation_Definitions.
+Require Import Coq.Classes.RelationClasses.
 Require Export Coq.Classes.Morphisms.
-Require Export Coq.Classes.SetoidTactics.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
 
+Open Local Scope signature_scope.
+
 (** Every [Equivalence] gives a default relation, if no other is given (lowest priority). *)
 
 Instance [ ! Equivalence A R ] => 
@@ -35,16 +37,16 @@ Definition equiv [ Equivalence A R ] : relation A := R.
 
 (** Shortcuts to make proof search possible (unification won't unfold equiv). *)
 
-Program Instance [ sa : ! Equivalence A ] => equiv_refl : reflexive equiv.
+Program Instance [ sa : ! Equivalence A ] => equiv_refl : Reflexive equiv.
 
-Program Instance [ sa : ! Equivalence A ] => equiv_sym : symmetric equiv.
+Program Instance [ sa : ! Equivalence A ] => equiv_sym : Symmetric equiv.
 
   Next Obligation.
   Proof.
     symmetry ; auto.
   Qed.
 
-Program Instance [ sa : ! Equivalence A ] => equiv_trans : transitive equiv.
+Program Instance [ sa : ! Equivalence A ] => equiv_trans : Transitive equiv.
 
   Next Obligation.
   Proof.
@@ -112,12 +114,12 @@ Ltac equivify_tac :=
 
 Ltac equivify := repeat equivify_tac.
 
-(** Every equivalence relation gives rise to a morphism, as it is transitive and symmetric. *)
+(** Every equivalence relation gives rise to a morphism, as it is Transitive and Symmetric. *)
 
 Instance [ sa : ! Equivalence ] => equiv_morphism : Morphism (equiv ++> equiv ++> iff) equiv :=
   respect := respect.
 
-(** The partial application too as it is reflexive. *)
+(** The partial application too as it is Reflexive. *)
 
 Instance [ sa : ! Equivalence A ] (x : A) => 
   equiv_partial_app_morphism : Morphism (equiv ++> iff) (equiv x) :=
diff --git a/theories/Classes/Functions.v b/theories/Classes/Functions.v
index 2795e4218..28fa55ee1 100644
--- a/theories/Classes/Functions.v
+++ b/theories/Classes/Functions.v
@@ -15,9 +15,8 @@
 
 (* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)
 
-Require Import Coq.Program.Program.
-Require Export Coq.Classes.RelationClasses.
-Require Export Coq.Classes.Morphisms.
+Require Import Coq.Classes.RelationClasses.
+Require Import Coq.Classes.Morphisms.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index c752cae86..f4ec50989 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -17,6 +17,7 @@
 
 Require Import Coq.Program.Basics.
 Require Import Coq.Program.Tactics.
+Require Import Coq.Relations.Relation_Definitions.
 Require Export Coq.Classes.RelationClasses.
 
 Set Implicit Arguments.
@@ -38,9 +39,20 @@ Definition respectful A B (R : relation A) (R' : relation B) : relation (A -> B)
 
 (** Notations reminiscent of the old syntax for declaring morphisms. *)
 
-Notation " R ++> R' " := (@respectful _ _ R R') (right associativity, at level 20).
-Notation " R ==> R' " := (@respectful _ _ R R') (right associativity, at level 20).
-Notation " R --> R' " := (@respectful _ _ (inverse R) R') (right associativity, at level 20).
+Delimit Scope signature_scope with signature.
+
+Notation " R ++> R' " := (@respectful _ _ (R%signature) (R'%signature)) 
+  (right associativity, at level 55) : signature_scope.
+
+Notation " R ==> R' " := (@respectful _ _ (R%signature) (R'%signature))
+  (right associativity, at level 55) : signature_scope.
+
+Notation " R --> R' " := (@respectful _ _ (inverse (R%signature)) (R'%signature))
+  (right associativity, at level 55) : signature_scope.
+
+Arguments Scope respectful [type_scope type_scope signature_scope signature_scope].
+
+Open Local Scope signature_scope.
 
 (** A morphism on a relation [R] is an object respecting the relation (in its kernel). 
    The relation [R] will be instantiated by [respectful] and [A] by an arrow type 
@@ -49,6 +61,8 @@ Notation " R --> R' " := (@respectful _ _ (inverse R) R') (right associativity,
 Class Morphism A (R : relation A) (m : A) : Prop :=
   respect : R m m.
 
+Arguments Scope Morphism [type_scope signature_scope].
+
 (** Here we build an equivalence instance for functions which relates respectful ones only. *)
 
 Definition respecting [ Equivalence A (R : relation A), Equivalence B (R' : relation B) ] : Type := 
@@ -163,7 +177,7 @@ Program Instance iff_iff_iff_impl_morphism : Morphism (iff ==> iff ==> iff) impl
 
 (* Typeclasses eauto := debug. *)
 
-Program Instance [ ! symmetric A R, Morphism (R ==> impl) m ] => reflexive_impl_iff : Morphism (R ==> iff) m.
+Program Instance [ ! Symmetric A R, Morphism (R ==> impl) m ] => Reflexive_impl_iff : Morphism (R ==> iff) m.
 
   Next Obligation.
   Proof.
@@ -202,10 +216,10 @@ Program Instance {A B C : Type} [ Morphism (RA ==> RB ==> RC) (f : A -> B -> C)
     apply respect ; auto.
   Qed.
 
-(** Every transitive relation gives rise to a binary morphism on [impl], 
+(** Every Transitive relation gives rise to a binary morphism on [impl], 
    contravariant in the first argument, covariant in the second. *)
 
-Program Instance [ ! transitive A (R : relation A) ] => 
+Program Instance [ ! Transitive A (R : relation A) ] => 
   trans_contra_co_morphism : Morphism (R --> R ++> impl) R.
 
   Next Obligation.
@@ -216,7 +230,7 @@ Program Instance [ ! transitive A (R : relation A) ] =>
 
 (** Dually... *)
 
-Program Instance [ ! transitive A (R : relation A) ] =>
+Program Instance [ ! Transitive A (R : relation A) ] =>
   trans_co_contra_inv_impl_morphism : Morphism (R ++> R --> inverse impl) R.
   
   Next Obligation.
@@ -224,7 +238,7 @@ Program Instance [ ! transitive A (R : relation A) ] =>
     apply* trans_contra_co_morphism ; eauto. eauto.
   Qed.
 
-(* Program Instance [ transitive A (R : relation A), symmetric A R ] => *)
+(* Program Instance [ Transitive A (R : relation A), Symmetric A R ] => *)
 (*   trans_sym_contra_co_inv_impl_morphism : ? Morphism (R --> R ++> inverse impl) R. *)
 
 (*   Next Obligation. *)
@@ -238,7 +252,7 @@ Program Instance [ ! transitive A (R : relation A) ] =>
 
 (** Morphism declarations for partial applications. *)
 
-Program Instance [ ! transitive A R ] (x : A) =>
+Program Instance [ ! Transitive A R ] (x : A) =>
   trans_contra_inv_impl_morphism : Morphism (R --> inverse impl) (R x).
 
   Next Obligation.
@@ -246,7 +260,7 @@ Program Instance [ ! transitive A R ] (x : A) =>
     transitivity y...
   Qed.
 
-Program Instance [ ! transitive A R ] (x : A) =>
+Program Instance [ ! Transitive A R ] (x : A) =>
   trans_co_impl_morphism : Morphism (R ==> impl) (R x).
 
   Next Obligation.
@@ -254,7 +268,7 @@ Program Instance [ ! transitive A R ] (x : A) =>
     transitivity x0...
   Qed.
 
-Program Instance [ ! transitive A R, symmetric R ] (x : A) =>
+Program Instance [ ! Transitive A R, Symmetric R ] (x : A) =>
   trans_sym_co_inv_impl_morphism : Morphism (R ==> inverse impl) (R x).
 
   Next Obligation.
@@ -262,7 +276,7 @@ Program Instance [ ! transitive A R, symmetric R ] (x : A) =>
     transitivity y...
   Qed.
 
-Program Instance [ ! transitive A R, symmetric R ] (x : A) =>
+Program Instance [ ! Transitive A R, Symmetric R ] (x : A) =>
   trans_sym_contra_impl_morphism : Morphism (R --> impl) (R x).
 
   Next Obligation.
@@ -281,10 +295,10 @@ Program Instance [ Equivalence A R ] (x : A) =>
     symmetry...
   Qed.
 
-(** With symmetric relations, variance is no issue ! *)
+(** With Symmetric relations, variance is no issue ! *)
 
 (* Program Instance (A B : Type) (R : relation A) (R' : relation B) *)
-(*   [ Morphism _ (R ==> R') m ] [ symmetric A R ] =>  *)
+(*   [ Morphism _ (R ==> R') m ] [ Symmetric A R ] =>  *)
 (*   sym_contra_morphism : Morphism (R --> R') m. *)
 
 (*   Next Obligation. *)
@@ -293,16 +307,16 @@ Program Instance [ Equivalence A R ] (x : A) =>
 (*     sym... *)
 (*   Qed. *)
 
-(** [R] is reflexive, hence we can build the needed proof. *)
+(** [R] is Reflexive, hence we can build the needed proof. *)
 
 Program Instance (A B : Type) (R : relation A) (R' : relation B)
-  [ Morphism (R ==> R') m ] [ reflexive R ] (x : A) =>
-  reflexive_partial_app_morphism : Morphism R' (m x) | 3.
+  [ Morphism (R ==> R') m ] [ Reflexive R ] (x : A) =>
+  Reflexive_partial_app_morphism : Morphism R' (m x) | 3.
 
-(** Every transitive relation induces a morphism by "pushing" an [R x y] on the left of an [R x z] proof
+(** Every Transitive relation induces a morphism by "pushing" an [R x y] on the left of an [R x z] proof
    to get an [R y z] goal. *)
 
-Program Instance [ ! transitive A R ] => 
+Program Instance [ ! Transitive A R ] => 
   trans_co_eq_inv_impl_morphism : Morphism (R ==> (@eq A) ==> inverse impl) R.
 
   Next Obligation.
@@ -310,7 +324,7 @@ Program Instance [ ! transitive A R ] =>
     transitivity y...
   Qed.
 
-Program Instance [ ! transitive A R ] => 
+Program Instance [ ! Transitive A R ] => 
   trans_contra_eq_impl_morphism : Morphism (R --> (@eq A) ==> impl) R.
 
   Next Obligation.
@@ -318,9 +332,9 @@ Program Instance [ ! transitive A R ] =>
     transitivity x...
   Qed.
 
-(** Every symmetric and transitive relation gives rise to an equivariant morphism. *)
+(** Every Symmetric and Transitive relation gives rise to an equivariant morphism. *)
 
-Program Instance [ ! transitive A R, symmetric R ] => 
+Program Instance [ ! Transitive A R, Symmetric R ] => 
   trans_sym_morphism : Morphism (R ==> R ==> iff) R.
 
   Next Obligation.
@@ -407,12 +421,12 @@ Program Instance or_iff_morphism :
 (*   red ; intros. subst ; split; trivial. *)
 (* Qed. *)
 
-Instance (A B : Type) [ ! reflexive B R ] (m : A -> B) =>
-  eq_reflexive_morphism : Morphism (@Logic.eq A ==> R) m | 3.
+Instance (A B : Type) [ ! Reflexive B R ] (m : A -> B) =>
+  eq_Reflexive_morphism : Morphism (@Logic.eq A ==> R) m | 3.
 Proof. simpl_relation. Qed.
 
-Instance (A B : Type) [ ! reflexive B R' ] => 
-  reflexive (@Logic.eq A ==> R').
+Instance (A B : Type) [ ! Reflexive B R' ] => 
+  Reflexive (@Logic.eq A ==> R').
 Proof. simpl_relation. Qed.
 
 (** [respectful] is a morphism for relation equivalence. *)
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 53079674f..492b8498a 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -50,74 +50,74 @@ Proof. reflexivity. Qed.
 
 (** We rebind relations in separate classes to be able to overload each proof. *)
 
-Class reflexive A (R : relation A) :=
+Class Reflexive A (R : relation A) :=
   reflexivity : forall x, R x x.
 
-Class irreflexive A (R : relation A) := 
+Class Irreflexive A (R : relation A) := 
   irreflexivity : forall x, R x x -> False.
 
-Class symmetric A (R : relation A) := 
+Class Symmetric A (R : relation A) := 
   symmetry : forall x y, R x y -> R y x.
 
-Class asymmetric A (R : relation A) := 
+Class Asymmetric A (R : relation A) := 
   asymmetry : forall x y, R x y -> R y x -> False.
 
-Class transitive A (R : relation A) := 
+Class Transitive A (R : relation A) := 
   transitivity : forall x y z, R x y -> R y z -> R x z.
 
-Implicit Arguments reflexive [A].
-Implicit Arguments irreflexive [A].
-Implicit Arguments symmetric [A].
-Implicit Arguments asymmetric [A].
-Implicit Arguments transitive [A].
+Implicit Arguments Reflexive [A].
+Implicit Arguments Irreflexive [A].
+Implicit Arguments Symmetric [A].
+Implicit Arguments Asymmetric [A].
+Implicit Arguments Transitive [A].
 
 Hint Resolve @irreflexivity : ord.
 
 (** We can already dualize all these properties. *)
 
-Program Instance [ ! reflexive A R ] => flip_reflexive : reflexive (flip R) :=
+Program Instance [ ! Reflexive A R ] => flip_Reflexive : Reflexive (flip R) :=
   reflexivity := reflexivity (R:=R).
 
-Program Instance [ ! irreflexive A R ] => flip_irreflexive : irreflexive (flip R) :=
+Program Instance [ ! Irreflexive A R ] => flip_Irreflexive : Irreflexive (flip R) :=
   irreflexivity := irreflexivity (R:=R).
 
-Program Instance [ ! symmetric A R ] => flip_symmetric : symmetric (flip R).
+Program Instance [ ! Symmetric A R ] => flip_Symmetric : Symmetric (flip R).
 
-  Solve Obligations using unfold flip ; program_simpl ; clapply symmetric.
+  Solve Obligations using unfold flip ; program_simpl ; clapply Symmetric.
 
-Program Instance [ ! asymmetric A R ] => flip_asymmetric : asymmetric (flip R).
+Program Instance [ ! Asymmetric A R ] => flip_Asymmetric : Asymmetric (flip R).
   
   Solve Obligations using program_simpl ; unfold flip in * ; intros ; clapply asymmetry.
 
-Program Instance [ ! transitive A R ] => flip_transitive : transitive (flip R).
+Program Instance [ ! Transitive A R ] => flip_Transitive : Transitive (flip R).
 
   Solve Obligations using unfold flip ; program_simpl ; clapply transitivity.
 
 (** Have to do it again for Prop. *)
 
-Program Instance [ ! reflexive A (R : relation A) ] => inverse_reflexive : reflexive (inverse R) :=
+Program Instance [ ! Reflexive A (R : relation A) ] => inverse_Reflexive : Reflexive (inverse R) :=
   reflexivity := reflexivity (R:=R).
 
-Program Instance [ ! irreflexive A (R : relation A) ] => inverse_irreflexive : irreflexive (inverse R) :=
+Program Instance [ ! Irreflexive A (R : relation A) ] => inverse_Irreflexive : Irreflexive (inverse R) :=
   irreflexivity := irreflexivity (R:=R).
 
-Program Instance [ ! symmetric A (R : relation A) ] => inverse_symmetric : symmetric (inverse R).
+Program Instance [ ! Symmetric A (R : relation A) ] => inverse_Symmetric : Symmetric (inverse R).
 
-  Solve Obligations using unfold inverse, flip ; program_simpl ; clapply symmetric.
+  Solve Obligations using unfold inverse, flip ; program_simpl ; clapply Symmetric.
 
-Program Instance [ ! asymmetric A (R : relation A) ] => inverse_asymmetric : asymmetric (inverse R).
+Program Instance [ ! Asymmetric A (R : relation A) ] => inverse_Asymmetric : Asymmetric (inverse R).
   
   Solve Obligations using program_simpl ; unfold inverse, flip in * ; intros ; clapply asymmetry.
 
-Program Instance [ ! transitive A (R : relation A) ] => inverse_transitive : transitive (inverse R).
+Program Instance [ ! Transitive A (R : relation A) ] => inverse_Transitive : Transitive (inverse R).
 
   Solve Obligations using unfold inverse, flip ; program_simpl ; clapply transitivity.
 
-Program Instance [ ! reflexive A (R : relation A) ] => 
-  reflexive_complement_irreflexive : irreflexive (complement R).
+Program Instance [ ! Reflexive A (R : relation A) ] => 
+  Reflexive_complement_Irreflexive : Irreflexive (complement R).
 
-Program Instance [ ! irreflexive A (R : relation A) ] => 
-  irreflexive_complement_reflexive : reflexive (complement R).
+Program Instance [ ! Irreflexive A (R : relation A) ] => 
+  Irreflexive_complement_Reflexive : Reflexive (complement R).
 
   Next Obligation. 
   Proof. 
@@ -125,7 +125,7 @@ Program Instance [ ! irreflexive A (R : relation A) ] =>
     apply (irreflexivity H).
   Qed.
 
-Program Instance [ ! symmetric A (R : relation A) ] => complement_symmetric : symmetric (complement R).
+Program Instance [ ! Symmetric A (R : relation A) ] => complement_Symmetric : Symmetric (complement R).
 
   Next Obligation.
   Proof.
@@ -155,34 +155,34 @@ Ltac obligations_tactic ::= simpl_relation.
 
 (** Logical implication. *)
 
-Program Instance impl_refl : reflexive impl.
-Program Instance impl_trans : transitive impl.
+Program Instance impl_refl : Reflexive impl.
+Program Instance impl_trans : Transitive impl.
 
 (** Logical equivalence. *)
 
-Program Instance iff_refl : reflexive iff.
-Program Instance iff_sym : symmetric iff.
-Program Instance iff_trans : transitive iff.
+Program Instance iff_refl : Reflexive iff.
+Program Instance iff_sym : Symmetric iff.
+Program Instance iff_trans : Transitive iff.
 
 (** Leibniz equality. *)
 
-Program Instance eq_refl : reflexive (@eq A).
-Program Instance eq_sym : symmetric (@eq A).
-Program Instance eq_trans : transitive (@eq A).
+Program Instance eq_refl : Reflexive (@eq A).
+Program Instance eq_sym : Symmetric (@eq A).
+Program Instance eq_trans : Transitive (@eq A).
 
 (** Various combinations of reflexivity, symmetry and transitivity. *)
 
-(** A [PreOrder] is both reflexive and transitive. *)
+(** A [PreOrder] is both Reflexive and Transitive. *)
 
 Class PreOrder A (R : relation A) :=
-  preorder_refl :> reflexive R ;
-  preorder_trans :> transitive R.
+  preorder_refl :> Reflexive R ;
+  preorder_trans :> Transitive R.
 
-(** A partial equivalence relation is symmetric and transitive. *)
+(** A partial equivalence relation is Symmetric and Transitive. *)
 
 Class PER (carrier : Type) (pequiv : relation carrier) :=
-  per_sym :> symmetric pequiv ;
-  per_trans :> transitive pequiv.
+  per_sym :> Symmetric pequiv ;
+  per_trans :> Transitive pequiv.
 
 (** We can build a PER on the Coq function space if we have PERs on the domain and
    codomain. *)
@@ -201,20 +201,20 @@ Program Instance [ PER A (R : relation A), PER B (R' : relation B) ] =>
 (** The [Equivalence] typeclass. *)
 
 Class Equivalence (carrier : Type) (equiv : relation carrier) :=
-  equiv_refl :> reflexive equiv ;
-  equiv_sym :> symmetric equiv ;
-  equiv_trans :> transitive equiv.
+  equiv_refl :> Reflexive equiv ;
+  equiv_sym :> Symmetric equiv ;
+  equiv_trans :> Transitive equiv.
 
 (** We can now define antisymmetry w.r.t. an equivalence relation on the carrier. *)
 
-Class [ Equivalence A eqA ] => antisymmetric (R : relation A) := 
+Class [ Equivalence A eqA ] => Antisymmetric (R : relation A) := 
   antisymmetry : forall x y, R x y -> R y x -> eqA x y.
 
-Program Instance [ eq : Equivalence A eqA, antisymmetric eq R ] => 
-  flip_antisymmetric : antisymmetric eq (flip R).
+Program Instance [ eq : Equivalence A eqA, Antisymmetric eq R ] => 
+  flip_antiSymmetric : Antisymmetric eq (flip R).
 
-Program Instance [ eq : Equivalence A eqA, antisymmetric eq (R : relation A) ] => 
-  inverse_antisymmetric : antisymmetric eq (inverse R).
+Program Instance [ eq : Equivalence A eqA, Antisymmetric eq (R : relation A) ] => 
+  inverse_antiSymmetric : Antisymmetric eq (inverse R).
 
 (** Leibinz equality [eq] is an equivalence relation. *)
 
diff --git a/theories/Classes/SetoidAxioms.v b/theories/Classes/SetoidAxioms.v
index 6b7881c9f..7cf2980c4 100644
--- a/theories/Classes/SetoidAxioms.v
+++ b/theories/Classes/SetoidAxioms.v
@@ -32,4 +32,4 @@ Axiom setoideq_eq : forall [ sa : Setoid a ] (x y : a), x == y -> x = y.
 Ltac setoid_extensionality :=
   match goal with
     [ |- @eq ?A ?X ?Y ] => apply (setoideq_eq (a:=A) (x:=X) (y:=Y))
-  end.
\ No newline at end of file
+  end.
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index d2ee4f443..e64cbd12c 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -15,15 +15,15 @@
 
 (* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)
 
-Require Import Coq.Program.Program.
-Require Import Coq.Classes.Init.
-
 Set Implicit Arguments.
 Unset Strict Implicit.
 
+Require Import Coq.Program.Program.
+
+Require Import Coq.Classes.Init.
 Require Export Coq.Classes.RelationClasses.
 Require Export Coq.Classes.Morphisms.
-Require Export Coq.Classes.Functions.
+Require Import Coq.Classes.Functions.
 
 (** A setoid wraps an equivalence. *)
 
@@ -40,13 +40,13 @@ Typeclasses unfold @equiv.
 
 (** Shortcuts to make proof search easier. *)
 
-Definition setoid_refl [ sa : Setoid A ] : reflexive equiv.
+Definition setoid_refl [ sa : Setoid A ] : Reflexive equiv.
 Proof. eauto with typeclass_instances. Qed.
 
-Definition setoid_sym [ sa : Setoid A ] : symmetric equiv.
+Definition setoid_sym [ sa : Setoid A ] : Symmetric equiv.
 Proof. eauto with typeclass_instances. Qed.
 
-Definition setoid_trans [ sa : Setoid A ] : transitive equiv.
+Definition setoid_trans [ sa : Setoid A ] : Transitive equiv.
 Proof. eauto with typeclass_instances. Qed.
 
 Existing Instance setoid_refl.
@@ -131,7 +131,7 @@ Implicit Arguments setoid_morphism [[!sa]].
 Existing Instance setoid_morphism.
 
 Program Definition setoid_partial_app_morphism [ sa : Setoid A ] (x : A) : Morphism (equiv ++> iff) (equiv x) :=
-  reflexive_partial_app_morphism.
+  Reflexive_partial_app_morphism.
 
 Existing Instance setoid_partial_app_morphism.
 
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index ee8c530fa..8d2be43cc 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -17,6 +17,8 @@
 
 Require Export Coq.Classes.RelationClasses.
 Require Export Coq.Classes.Morphisms.
+Require Export Coq.Classes.Equivalence.
+Require Export Coq.Relations.Relation_Definitions.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -65,6 +67,8 @@ Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id)
 
 Require Import Coq.Program.Tactics.
 
+Open Local Scope signature_scope.
+
 Ltac red_subst_eq_morphism concl :=
   match concl with
     | @Logic.eq ?A ==> ?R' => red ; intros ; subst ; red_subst_eq_morphism R'
diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v
index 34bff6354..983c651ab 100644
--- a/theories/Setoids/Setoid.v
+++ b/theories/Setoids/Setoid.v
@@ -10,8 +10,7 @@
 
 Set Implicit Arguments.
 
-Require Export Coq.Classes.Equivalence.
-Require Export Coq.Relations.Relation_Definitions.
+Require Export Coq.Classes.SetoidTactics.
 
 (** For backward compatibility *)