diff options
Diffstat (limited to 'test-suite/bugs/closed/bug_9583.v')
| -rw-r--r-- | test-suite/bugs/closed/bug_9583.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_9583.v b/test-suite/bugs/closed/bug_9583.v new file mode 100644 index 0000000000..14232e8578 --- /dev/null +++ b/test-suite/bugs/closed/bug_9583.v @@ -0,0 +1,7 @@ +(* Was causing a stack overflow before #11613 *) +Declare Custom Entry bla. +Notation "[ t ]" := (t) (at level 0, t custom bla at level 0). +Notation "] t [" := (t) (in custom bla at level 0, t custom bla at level 0). +Notation "t" := (t) (in custom bla at level 0, t constr at level 9). +Notation "0" := (0) (in custom bla at level 0). +Check fun x => [ ] x [ ]. |