diff options
| author | Hugo Herbelin | 2017-08-05 22:28:28 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-08-29 05:18:49 +0200 |
| commit | 7a9205cd226c1df6a52afaee3374bc9cdffd6e8c (patch) | |
| tree | 51bf7d93e321a6b177e18d2b5a9c0cc77bf6a00d | |
| parent | 12f4cb9c189bd70a6cd252a5269b6d3c7d327667 (diff) | |
Adding a test for #5569 (warning about skipping spaces).
The two previous commits make the warning irrelevant and useless.
| -rw-r--r-- | test-suite/output/Notations3.out | 2 | ||||
| -rw-r--r-- | test-suite/output/Notations3.v | 6 |
2 files changed, 8 insertions, 0 deletions
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index c66f801223..e5dbfcb4be 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -120,3 +120,5 @@ where letpair x [1] = {0}; return (1, 2, 3, 4) : nat * nat * nat * nat +{{ 1 | 1 // 1 }} + : nat diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 58f9e15abc..b1015137d6 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -180,3 +180,9 @@ Reserved Notation "'letpair' x [1] = { A } ; 'return' ( b0 , b1 , .. , b2 )" Notation "'letpair' x [1] = { a } ; 'return' ( b0 , b1 , .. , b2 )" := (let x:=a in ( .. (b0,b1) .., b2)). Check letpair x [1] = {0}; return (1,2,3,4). + +(* Test spacing in #5569 *) + +Notation "{ { xL | xR // xcut } }" := (xL+xR+xcut) + (at level 0, xR at level 39, format "{ { xL | xR // xcut } }"). +Check 1+1+1. |