From 96e486509a5d4d7cbee2589af32d18eaa07d8105 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 16 Mar 2011 14:52:59 +0000
Subject: Remove some weird syntax "fun ... ," that used to be accepted (cf
 r13876)

 Probably something related with the unicode lambda syntax...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13911 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/output/Notations2.v | 2 +-
 test-suite/success/Notations.v | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v
index 57d8ebbc47..a78088bad5 100644
--- a/test-suite/output/Notations2.v
+++ b/test-suite/output/Notations2.v
@@ -37,7 +37,7 @@ Notation "∀  x .. y , P":= (forall x, .. (forall y, P) ..)
 
 Check (∀ n p, n+p=0).
 
-Notation "'λ'  x .. y , P":= (fun x, .. (fun y, P) ..)
+Notation "'λ'  x .. y , P":= (fun x => .. (fun y => P) ..)
   (y binder, at level 200, right associativity).
 
 Check (λ n p, n+p=0).
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index 18e2479e50..6214062899 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -63,6 +63,6 @@ Check [ 0 # ; 1 ].
 (* Check well-scoping of alpha-renaming of private binders *)
 (* see bug #2248 (thanks to Marc Lasson) *)
 
-Notation "{ q , r | P }" := (fun (p:nat*nat), let (q, r) := p in P).
-Check (fun p, {q,r| q + r = p}).
+Notation "{ q , r | P }" := (fun (p:nat*nat) => let (q, r) := p in P).
+Check (fun p => {q,r| q + r = p}).
 
-- 
cgit v1.2.3