From 92696abcaab68c70461c285ada87e50dacf3bb34 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 8 Apr 2009 12:58:07 +0000
Subject: - 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
---
 test-suite/success/Notations.v | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index d3b3689527..84ff2608a2 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.
-- 
cgit v1.2.3