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

9 files changed, 158 insertions, 112 deletions

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 79faadca6..a3baa1abb 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -1,3 +1,4 @@
+(* -*- compile-command: "make -C .. bin/coqtop.byte" -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -423,6 +424,12 @@ let morphism_class =
 
 let respect_proj = lazy (mkConst (List.hd (Lazy.force morphism_class).cl_projs))
 
+let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
+
+let try_find_reference dir s =
+  let sp = Libnames.make_path (make_dir ("Coq"::dir)) (id_of_string s) in
+    constr_of_global (Nametab.absolute_reference sp)
+
 let gen_constant dir s = Coqlib.gen_constant "Class_setoid" dir s
 let coq_proj1 = lazy(gen_constant ["Init"; "Logic"] "proj1")
 let coq_proj2 = lazy(gen_constant ["Init"; "Logic"] "proj2")
@@ -431,14 +438,14 @@ let impl = lazy (gen_constant ["Program"; "Basics"] "impl")
 let arrow = lazy (gen_constant ["Program"; "Basics"] "arrow")
 let coq_id = lazy (gen_constant ["Program"; "Basics"] "id")
 
-let reflexive_type = lazy (gen_constant ["Classes"; "RelationClasses"] "reflexive")
-let reflexive_proof = lazy (gen_constant ["Classes"; "RelationClasses"] "reflexivity")
+let reflexive_type = lazy (try_find_reference ["Classes"; "RelationClasses"] "Reflexive")
+let reflexive_proof = lazy (try_find_reference ["Classes"; "RelationClasses"] "reflexivity")
 
-let symmetric_type = lazy (gen_constant ["Classes"; "RelationClasses"] "symmetric")
-let symmetric_proof = lazy (gen_constant ["Classes"; "RelationClasses"] "symmetry")
+let symmetric_type = lazy (try_find_reference ["Classes"; "RelationClasses"] "Symmetric")
+let symmetric_proof = lazy (try_find_reference ["Classes"; "RelationClasses"] "symmetry")
 
-let transitive_type = lazy (gen_constant ["Classes"; "RelationClasses"] "transitive")
-let transitive_proof = lazy (gen_constant ["Classes"; "RelationClasses"] "transitivity")
+let transitive_type = lazy (try_find_reference ["Classes"; "RelationClasses"] "Transitive")
+let transitive_proof = lazy (try_find_reference ["Classes"; "RelationClasses"] "transitivity")
 
 let inverse = lazy (gen_constant ["Classes"; "RelationClasses"] "inverse")
 let complement = lazy (gen_constant ["Classes"; "RelationClasses"] "complement")
@@ -524,13 +531,13 @@ let reflexivity_proof_evar env evars carrier relation x =
 (* 	mkCast (mkMeta meta, DEFAULTcast, mkApp (relation, [| x; x |])) *)
 
 let find_class_proof proof_type proof_method env carrier relation =
-  let goal =
-    mkApp (Lazy.force proof_type, [| carrier ; relation |])
-  in
-    try 
-      let inst = resolve_one_typeclass env goal in
-	mkApp (Lazy.force proof_method, [| carrier ; relation ; inst |])
-    with e when Logic.catchable_exception e -> raise Not_found
+  try 
+    let goal =
+      mkApp (Lazy.force proof_type, [| carrier ; relation |])
+    in
+    let inst = resolve_one_typeclass env goal in
+      mkApp (Lazy.force proof_method, [| carrier ; relation ; inst |])
+  with e when Logic.catchable_exception e -> raise Not_found
 
 let reflexive_proof env = find_class_proof reflexive_type reflexive_proof env
 let symmetric_proof env = find_class_proof symmetric_type symmetric_proof env
@@ -986,17 +993,17 @@ let init_setoid () =
   check_required_library ["Coq";"Setoids";"Setoid"]
 
 let declare_instance_refl a aeq n lemma = 
-  let instance = declare_instance a aeq (add_suffix n "_refl") "Coq.Classes.RelationClasses.reflexive" 
+  let instance = declare_instance a aeq (add_suffix n "_refl") "Coq.Classes.RelationClasses.Reflexive" 
   in anew_instance instance 
        [((dummy_loc,id_of_string "reflexivity"),[],lemma)]
 
 let declare_instance_sym a aeq n lemma = 
-  let instance = declare_instance a aeq (add_suffix n "_sym") "Coq.Classes.RelationClasses.symmetric"
+  let instance = declare_instance a aeq (add_suffix n "_sym") "Coq.Classes.RelationClasses.Symmetric"
   in anew_instance instance 
        [((dummy_loc,id_of_string "symmetry"),[],lemma)]
 
 let declare_instance_trans a aeq n lemma = 
-  let instance = declare_instance a aeq (add_suffix n "_trans") "Coq.Classes.RelationClasses.transitive" 
+  let instance = declare_instance a aeq (add_suffix n "_trans") "Coq.Classes.RelationClasses.Transitive" 
   in anew_instance instance 
        [((dummy_loc,id_of_string "transitivity"),[],lemma)]
 
@@ -1302,6 +1309,15 @@ let relation_of_constr c =
 	  mkApp (f, relargs), args
     | _ -> error "Not an applied relation"
 
+let is_loaded d =
+  let d' = List.map id_of_string d in
+  let dir = make_dirpath (List.rev d') in
+    Library.library_is_loaded dir
+
+let try_loaded f gl =
+  if is_loaded ["Coq";"Classes";"RelationClasses"] then f gl 
+  else tclFAIL 0 (str"You need to require Coq.Classes.RelationClasses first") gl
+    
 let setoid_reflexivity gl =
   let env = pf_env gl in
   let rel, args = relation_of_constr (pf_concl gl) in
@@ -1311,6 +1327,9 @@ let setoid_reflexivity gl =
       tclFAIL 0 (str" The relation " ++ Printer.pr_constr_env env rel ++ str" is not a declared reflexive relation")
 	gl
 
+(* let setoid_reflexivity gl = *)
+(*   try_loaded setoid_reflexivity gl *)
+	  
 let setoid_symmetry gl =
   let env = pf_env gl in
   let rel, args = relation_of_constr (pf_concl gl) in
@@ -1319,6 +1338,9 @@ let setoid_symmetry gl =
     with Not_found -> 
       tclFAIL 0 (str" The relation " ++ Printer.pr_constr_env env rel ++ str" is not a declared symmetric relation")
 	gl
+
+(* let setoid_symmetry gl = *)
+(*   try_loaded setoid_symmetry gl *)
 	
 let setoid_transitivity c gl =
   let env = pf_env gl in
@@ -1331,6 +1353,9 @@ let setoid_transitivity c gl =
       tclFAIL 0
 	(str" The relation " ++ Printer.pr_constr_env env rel ++ str" is not a declared transitive relation") gl
 	
+(* let setoid_transitivity c gl = *)
+(*   try_loaded (setoid_transitivity c) gl *)
+
 let setoid_symmetry_in id gl =
   let ctype = pf_type_of gl (mkVar id) in
   let binders,concl = Sign.decompose_prod_assum ctype in
@@ -1349,6 +1374,9 @@ let setoid_symmetry_in id gl =
 	tclTHENLIST [ intros; setoid_symmetry; apply (mkVar id); Tactics.assumption ] ]
       gl
 
+(* let setoid_symmetry_in h gl = *)
+(*   try_loaded (setoid_symmetry_in h) gl *)
+
 let _ = Tactics.register_setoid_reflexivity setoid_reflexivity
 let _ = Tactics.register_setoid_symmetry setoid_symmetry
 let _ = Tactics.register_setoid_symmetry_in setoid_symmetry_in
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 *)