Only export the notations of Morphism as well as Equivalence through

Setoid, the rest needs to be qualified.


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

2 files changed, 16 insertions, 13 deletions

diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index a95ee8570..d2bc277e9 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-name: "~/research/coq/trunk/bin/coqtop.byte"; coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.Morphisms"); compile-command: "make -C ../.. TIME='time -p'" -*- *)
+(* -*- coq-prog-name: "~/research/coq/trunk/bin/coqtop.byte"; coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.Morphisms"); compile-command: "make -C ../.. -j3 TIME='time -p'" -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -55,18 +55,24 @@ Definition respectful {A B : Type}
 (** Notations reminiscent of the old syntax for declaring morphisms. *)
 
 Delimit Scope signature_scope with signature.
+
 Arguments Scope Morphism [type_scope signature_scope].
+Arguments Scope respectful [type_scope type_scope signature_scope signature_scope].
 
-Notation " R ++> R' " := (@respectful _ _ (R%signature) (R'%signature)) 
-  (right associativity, at level 55) : signature_scope.
+Module MorphismNotations.
 
-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 _ _ (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.
 
-Notation " R --> R' " := (@respectful _ _ (inverse (R%signature)) (R'%signature))
-  (right associativity, at level 55) : signature_scope.
+End MorphismNotations.
 
-Arguments Scope respectful [type_scope type_scope signature_scope signature_scope].
+Export MorphismNotations.
 
 Open Local Scope signature_scope.
 
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index 70c8d6907..824543577 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -15,11 +15,8 @@
 
 (* $Id$ *)
 
-Require Export Coq.Classes.RelationClasses.
-Require Export Coq.Classes.Morphisms.
-Require Export Coq.Classes.Morphisms_Prop.
-Require Export Coq.Classes.Equivalence.
-Require Export Coq.Relations.Relation_Definitions.
+Require Import Coq.Classes.RelationClasses Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop.
+Require Export Coq.Classes.Equivalence Coq.Relations.Relation_Definitions.
 
 Set Implicit Arguments.
 Unset Strict Implicit.