diff options
| author | Hugo Herbelin | 2017-11-25 12:14:59 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2018-12-04 11:50:02 +0100 |
| commit | 93a65415ff582d2ceb5bb9d994edaa6068da8280 (patch) | |
| tree | 630333b9518caa8f7b97b9f1c32deba2ebf35aff /test-suite | |
| parent | fe81b1a6f813fe21f0cc21ede761acae64c7b026 (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 180e8d337e..421ec987ff 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). |