6 files changed, 20 insertions, 10 deletions
diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v
index aa653de0f..aa5a1f287 100644
--- a/theories/Classes/EquivDec.v
+++ b/theories/Classes/EquivDec.v
@@ -145,3 +145,8 @@ Program Instance list_eqdec `(eqa : EqDec A eq) : ! EqDec (list A) eq :=
     end }.
 
   Solve Obligations using unfold equiv, complement in * ; program_simpl ; intuition (discriminate || eauto).
+
+
+  Next Obligation. destruct x ; destruct y ; intuition eauto. Defined.
+
+  Solve Obligations using unfold equiv, complement in * ; program_simpl ; intuition (discriminate || eauto).
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index 3fcbac061..100ddbe3e 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -14,13 +14,13 @@
 
 (* $Id$ *)
 
-Require Export Coq.Program.Basics.
+Require Import Coq.Program.Basics.
 Require Import Coq.Program.Tactics.
 
 Require Import Coq.Classes.Init.
 Require Import Relation_Definitions.
-Require Import Coq.Classes.RelationClasses.
-Require Export Coq.Classes.Morphisms.
+Require Export Coq.Classes.RelationClasses.
+Require Import Coq.Classes.Morphisms.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index 824543577..9e66ef2a0 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -15,8 +15,11 @@
 
 (* $Id$ *)
 
-Require Import Coq.Classes.RelationClasses Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop.
-Require Export Coq.Classes.Equivalence Coq.Relations.Relation_Definitions.
+Require Import Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop.
+Require Export Coq.Classes.RelationClasses Coq.Relations.Relation_Definitions.
+Require Import Coq.Classes.Equivalence Coq.Program.Basics.
+
+Export MorphismNotations.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index f812ece9c..58e81f357 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -15,7 +15,7 @@
   different styles: equivalence and boolean equalities. 
 *)
 
-Require Import Bool DecidableType DecidableTypeEx OrderedType.
+Require Import Bool DecidableType DecidableTypeEx OrderedType Morphisms.
 Require Export FMapInterface. 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/theories/FSets/FSetFacts.v b/theories/FSets/FSetFacts.v
index 075bb81ba..c99107939 100644
--- a/theories/FSets/FSetFacts.v
+++ b/theories/FSets/FSetFacts.v
@@ -17,7 +17,7 @@
 *)
 
 Require Import DecidableTypeEx.
-Require Export FSetInterface. 
+Require Export FSetInterface.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
@@ -424,14 +424,14 @@ Add Relation t Subset
  transitivity proved by Subset_trans
  as SubsetSetoid.
 
-Instance In_s_m : Morphism (E.eq ==> Subset ++> impl) In | 1.
+Instance In_s_m : Morphisms.Morphism (E.eq ==> Subset ++> Basics.impl) In | 1.
 Proof.
   simpl_relation. eauto with set.
 Qed.
 
-Add Morphism Empty with signature Subset --> impl as Empty_s_m.
+Add Morphism Empty with signature Subset --> Basics.impl as Empty_s_m.
 Proof.
-unfold Subset, Empty, impl; firstorder.
+unfold Subset, Empty, Basics.impl; firstorder.
 Qed.
 
 Add Morphism add with signature E.eq ==> Subset ++> Subset as add_s_m.
diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v
index 613cabbd0..8d241d894 100644
--- a/theories/Setoids/Setoid.v
+++ b/theories/Setoids/Setoid.v
@@ -10,6 +10,8 @@
 
 Require Export Coq.Classes.SetoidTactics.
 
+Export Morphisms.MorphismNotations.
+
 (** For backward compatibility *)
 
 Definition Setoid_Theory := @Equivalence.