diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-25 12:14:59 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-27 19:31:49 +0100 |
| commit | 97960e114e72bc38814e78a71f06aca4fdfc4512 (patch) | |
| tree | 469c33477a33834c549dacc1bd8d81913b96bd1e /test-suite | |
| parent | 437f20f0a1c2717cd7baae52e2ab20750dd9d4fb (diff) | |
Pre-isolating a notation test to avoid interferences.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Notations3.v | 4 |
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). |