diff options
Diffstat (limited to 'test-suite/output/NumeralNotations.v')
| -rw-r--r-- | test-suite/output/NumeralNotations.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/test-suite/output/NumeralNotations.v b/test-suite/output/NumeralNotations.v index 22aff36d67..31154d9f45 100644 --- a/test-suite/output/NumeralNotations.v +++ b/test-suite/output/NumeralNotations.v @@ -457,3 +457,10 @@ Module Test20. Check let v := 4%kt in v : ty. Check let v := 5%kt in v : ty. End Test20. + +Module Test21. + + Check 00001. + Check (-1_000)%Z. + +End Test21. |