diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-04-08 12:58:07 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-04-08 12:58:07 +0000 |
| commit | 92696abcaab68c70461c285ada87e50dacf3bb34 (patch) | |
| tree | 879c41374e123e6890bc078ca3dc8aa75c2b71de /test-suite/success/Notations.v | |
| parent | 231ab951f0da54d81c74afefc11a43be4057e662 (diff) | |
- Backport of 12053 (fixing parsing segfault bug #2087) and 12058 (fixing
Not_found bug in Theorem with) from V8.2 to trunk.
- Improving indentation in presence of tabulation and utf-8 when
reporting error messages with "^^^^^^".
- Updating a few svn:ignore properties.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12059 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success/Notations.v')
| -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. |