diff options
Diffstat (limited to 'test-suite/success')
| -rw-r--r-- | test-suite/success/Notations.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v index d3b368952..84ff2608a 100644 --- a/test-suite/success/Notations.v +++ b/test-suite/success/Notations.v @@ -36,3 +36,10 @@ Section A. Global Notation "'Z'" := O (at level 9). End A. Notation "$ x" := (id x) (at level 30). Check ($ 5). + +(* Check regression of bug #2087 *) + +Notation "'exists' x , P" := (x, P) + (at level 200, x ident, right associativity, only parsing). + +Definition foo P := let '(exists x, Q) := P in x = Q :> nat. |