diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-04-17 20:36:33 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-04-17 20:36:33 +0000 |
| commit | b878f1130e6eeffad311f3737331bccac9bf9e86 (patch) | |
| tree | 17b25ddd0ed30e6ab29f3c5dad984de5fef4366b /theories/Classes/Morphisms.v | |
| parent | f2a46998e4f791309d74445cf43981aedec28fd1 (diff) | |
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
Diffstat (limited to 'theories/Classes/Morphisms.v')
| -rw-r--r-- | theories/Classes/Morphisms.v | 22 |
1 files changed, 14 insertions, 8 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. |