diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-12 10:49:07 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-12 13:37:13 +0200 |
| commit | 305c70d55f8305e8cca8daf8796ff27a142332fe (patch) | |
| tree | 59a61d67f5fdc99534d96a8d7e3887d44e280b7d /test-suite/bugs/closed/2406.v | |
| parent | 666dbb093b09c37941cfb856cdf96fda09c3bac9 (diff) | |
In bug #2406, renouncing to test failure of parsing error.
(AFAIU, it is the table of supported unicode characters which has to
be upgraded anyway.)
Diffstat (limited to 'test-suite/bugs/closed/2406.v')
| -rw-r--r-- | test-suite/bugs/closed/2406.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/2406.v b/test-suite/bugs/closed/2406.v index d46fbabbb..1bd66ffcc 100644 --- a/test-suite/bugs/closed/2406.v +++ b/test-suite/bugs/closed/2406.v @@ -1,3 +1,6 @@ (* Check correct handling of unsupported notations *) Notation "''" := (fun x => x) (at level 20). + +(* This fails with a syntax error but it is not catched by Fail Fail Definition crash_the_rooster f := . +*) |