diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-09-06 13:27:45 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-09-06 13:27:45 +0000 |
commit | f402a7969a656eaf71f88c3413b991af1bbfab0a (patch) | |
tree | 9062dbbc1d226762fed5a9c324054c65de4002de /theories/Classes/Morphisms.v | |
parent | af29dd0dc131674d1cb0007d86b2c12500556aad (diff) |
Avoid registering λ and Π as keywords just for some private Local Notation
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14459 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Classes/Morphisms.v')
-rw-r--r-- | theories/Classes/Morphisms.v | 13 |
1 files changed, 4 insertions, 9 deletions
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index 9b8301a5d..9a555e256 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -21,12 +21,6 @@ Require Export Coq.Classes.RelationClasses. Generalizable All Variables. Local Obligation Tactic := simpl_relation. -Local Notation "'λ' x .. y , t" := (fun x => .. (fun y => t) ..) - (at level 200, x binder, y binder, right associativity). - -Local Notation "'Π' x .. y , P" := (forall x, .. (forall y, P) ..) - (at level 200, x binder, y binder, right associativity) : type_scope. - (** * Morphisms. We now turn to the definition of [Proper] and declare standard instances. @@ -123,15 +117,16 @@ Definition forall_def {A : Type} (B : A -> Type) : Type := forall x : A, B x. (** Dependent pointwise lifting of a relation on the range. *) -Definition forall_relation {A : Type} {B : A -> Type} (sig : Π a : A, relation (B a)) : relation (Π x : A, B x) := - λ f g, Π a : A, sig a (f a) (g a). +Definition forall_relation {A : Type} {B : A -> Type} + (sig : forall a, relation (B a)) : relation (forall x, B x) := + fun f g => forall a, sig a (f a) (g a). Arguments Scope forall_relation [type_scope type_scope signature_scope]. (** Non-dependent pointwise lifting *) Definition pointwise_relation (A : Type) {B : Type} (R : relation B) : relation (A -> B) := - Eval compute in forall_relation (B:=λ _, B) (λ _, R). + Eval compute in forall_relation (B:=fun _ => B) (fun _ => R). Lemma pointwise_pointwise A B (R : relation B) : relation_equivalence (pointwise_relation A R) (@eq A ==> R). |