summaryrefslogtreecommitdiff
path: root/test-suite/success/Notations.v
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-06-04 12:07:52 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2012-06-04 12:07:52 +0200
commit61dc740ed1c3780cccaec00d059a28f0d31d0052 (patch)
treed88d05baf35b9b09a034233300f35a694f9fa6c2 /test-suite/success/Notations.v
parent97fefe1fcca363a1317e066e7f4b99b9c1e9987b (diff)
Imported Upstream version 8.4~gamma0+really8.4beta2upstream/8.4_gamma0+really8.4beta2
Diffstat (limited to 'test-suite/success/Notations.v')
-rw-r--r--test-suite/success/Notations.v14
1 files changed, 12 insertions, 2 deletions
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index f5f5a9d1..89f11059 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -17,10 +17,12 @@ Check (nat |= nat --> nat).
(* Check that first non empty definition at an empty level can be of any
associativity *)
-Definition marker := O.
+Module Type v1.
Notation "x +1" := (S x) (at level 8, left associativity).
-Reset marker.
+End v1.
+Module Type v2.
Notation "x +1" := (S x) (at level 8, right associativity).
+End v2.
(* Check that empty levels (here 8 and 2 in pattern) are added in the
right order *)
@@ -86,3 +88,11 @@ Notation "'FOO' x" := (S x) (at level 40).
Goal (2 ++++ 3) = 5.
reflexivity.
Abort.
+
+(* Check correct failure handling when a non-constructor notation is
+ used in cases pattern (bug #2724 in 8.3 and 8.4beta) *)
+
+Notation "'FORALL' x .. y , P" := (forall x, .. (forall y, P) ..)
+ (at level 200, x binder, y binder, right associativity) : type_scope.
+
+Fail Check fun x => match x with S (FORALL x, _) => 0 end.