Just export RelationClasses for [Equivalence] through Setoid.

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

2 files changed, 5 insertions, 5 deletions

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.