From 22a8453f551349bbafa14b914aa784693dcf3615 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 20 Jan 2012 21:08:33 +0000
Subject: Notations with binders: Accepting using notations for functional
 terms which do not necessarily depend on their parameter (e.g. a notation for
 "fun x => t" might match also "fun _ => t").

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

(limited to 'test-suite')

diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out
index 47741e439a..3b3351d330 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -46,3 +46,7 @@ match n with
 | plus2 _ :: _ => 2
 end
      : list(nat) -> nat
+# x : nat => x
+     : nat -> nat
+# _ : nat => 2
+     : nat -> nat
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v
index e902a3c273..1fcbe858a8 100644
--- a/test-suite/output/Notations2.v
+++ b/test-suite/output/Notations2.v
@@ -83,3 +83,13 @@ Notation "'mylet' f [ x ; .. ; y ]  :=  t 'in' u":=
 
 Check mylet f [x;y;z;(a:bool)] := x+y+z+1 in f 0 1 2.
 *)
+
+(* Check notations for functional terms which do not necessarily
+   depend on their parameter *)
+(* Old request mentioned again on coq-club 20/1/2012 *)
+
+Notation "#  x : T => t" := (fun x : T => t)
+  (at level 0, t at level 200, x ident).
+
+Check # x : nat => x.
+Check # _ : nat => 2.
-- 
cgit v1.2.3