aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-06-26 18:40:11 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-07-26 15:03:31 +0200
commitada7875e95cba2f08902c55cfd3f69d6cc80cac3 (patch)
treef989fe34a04bfc803f5bd6449a198bd9558ee116 /test-suite
parent51d418636adf30bcf4e37a5b7b479a7d54dbedb2 (diff)
Adding support for recursive notations of the form "x , .. , y , z".
Since camlp5 parses from left, the last ", z" was parsed as part of an arbitrary long list of "x1 , .. , xn" and a syntax error was raised since an extra ", z" was still expected. We support this by translating "x , .. , y , z" into "x , y , .. , z" and reassembling the arguments appropriately after parsing.
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/output/Notations3.out6
-rw-r--r--test-suite/output/Notations3.v8
2 files changed, 14 insertions, 0 deletions
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index ffea0819a..a9ae74fd6 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -109,3 +109,9 @@ fun x : ?A => x === x
: forall x : ?A, x = x
where
?A : [x : ?A |- Type] (x cannot be used)
+{0, 1}
+ : nat * nat
+{0, 1, 2}
+ : nat * (nat * nat)
+{0, 1, 2, 3}
+ : nat * (nat * (nat * nat))
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index 250aecafd..dee0f70f7 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -160,3 +160,11 @@ End Bug4765.
Notation "x === x" := (eq_refl x) (only printing, at level 10).
Check (fun x => eq_refl x).
+
+(**********************************************************************)
+(* Test recursive notations with the recursive pattern repeated on the right *)
+
+Notation "{ x , .. , y , z }" := (pair x .. (pair y z) ..).
+Check {0,1}.
+Check {0,1,2}.
+Check {0,1,2,3}.