aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/Notations3.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/output/Notations3.v')
-rw-r--r--test-suite/output/Notations3.v7
1 files changed, 7 insertions, 0 deletions
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index ea372ad1a..8c7bbe591 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -190,3 +190,10 @@ Check 1+1+1.
(* 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).
Check !!! (x y:nat), True.
+
+(* Allow level for leftmost nonterminal when printing-only, BZ#5739 *)
+
+Notation "* x" := (id x) (only printing, at level 15, format "* x").
+Notation "x . y" := (x + y) (only printing, at level 20, x at level 14, left associativity, format "x . y").
+Check (((id 1) + 2) + 3).
+Check (id (1 + 2)).