aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-11-25 12:14:59 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-11-27 19:31:49 +0100
commit97960e114e72bc38814e78a71f06aca4fdfc4512 (patch)
tree469c33477a33834c549dacc1bd8d81913b96bd1e /test-suite
parent437f20f0a1c2717cd7baae52e2ab20750dd9d4fb (diff)
Pre-isolating a notation test to avoid interferences.
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/output/Notations3.v4
1 files changed, 4 insertions, 0 deletions
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index 8c7bbe591..1f142cf47 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -183,9 +183,13 @@ Check letpair x [1] = {0}; return (1,2,3,4).
(* Test spacing in #5569 *)
+Section S1.
+Variable plus : nat -> nat -> nat.
+Infix "+" := plus.
Notation "{ { xL | xR // xcut } }" := (xL+xR+xcut)
(at level 0, xR at level 39, format "{ { xL | xR // xcut } }").
Check 1+1+1.
+End S1.
(* Test presence of notation variables in the recursive parts (introduced in dfdaf4de) *)
Notation "!!! x .. y , b" := ((fun x => b), .. ((fun y => b), True) ..) (at level 200, x binder).