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

2 files changed, 11 insertions, 17 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).
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index 762b3fc7d..6708220ea 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.v
@@ -18,9 +18,6 @@ Unset Strict Implicit.
 
 Generalizable Variables A B .
 
-Local Notation "'λ'  x .. y , t" := (fun x => .. (fun y => t) ..)
-  (at level 200, x binder, y binder, right associativity).
-
 (** Export notations. *)
 
 Require Export Coq.Classes.SetoidClass.
@@ -93,7 +90,7 @@ Program Instance bool_eqdec : EqDec (eq_setoid bool) :=
   bool_dec.
 
 Program Instance unit_eqdec : EqDec (eq_setoid unit) :=
-  λ x y, in_left.
+  fun x y => in_left.
 
   Next Obligation.
   Proof.
@@ -101,8 +98,9 @@ Program Instance unit_eqdec : EqDec (eq_setoid unit) :=
     reflexivity.
   Qed.
 
-Program Instance prod_eqdec `(! EqDec (eq_setoid A), ! EqDec (eq_setoid B)) : EqDec (eq_setoid (prod A B)) :=
-  λ x y,
+Program Instance prod_eqdec `(! EqDec (eq_setoid A), ! EqDec (eq_setoid B))
+ : EqDec (eq_setoid (prod A B)) :=
+  fun x y =>
     let '(x1, x2) := x in
     let '(y1, y2) := y in
     if x1 == y1 then
@@ -115,8 +113,9 @@ Program Instance prod_eqdec `(! EqDec (eq_setoid A), ! EqDec (eq_setoid B)) : Eq
 (** Objects of function spaces with countable domains like bool
   have decidable equality. *)
 
-Program Instance bool_function_eqdec `(! EqDec (eq_setoid A)) : EqDec (eq_setoid (bool -> A)) :=
-  λ f g,
+Program Instance bool_function_eqdec `(! EqDec (eq_setoid A))
+ : EqDec (eq_setoid (bool -> A)) :=
+  fun f g =>
     if f true == g true then
       if f false == g false then in_left
       else in_right