diff options
| -rw-r--r-- | theories/Classes/Morphisms.v | 22 | ||||
| -rw-r--r-- | theories/Classes/SetoidTactics.v | 7 |
2 files changed, 16 insertions, 13 deletions
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index a95ee8570f..d2bc277e9f 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 70c8d69077..8245435774 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. |