From 7a7a09378e492b5b2dc87e3a8e502e842ca1faf5 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 6 Apr 2011 11:38:31 +0000
Subject: Add 'Existing Instances' declaration to declare multiple instances at
 once.

This is useful, for example, in declaring the projection of the dependent
record bundled form of an unbundled typeclass.

Patch submitted by Tom Prince

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13956 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 ide/coq_lex.mll | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'ide')

diff --git a/ide/coq_lex.mll b/ide/coq_lex.mll
index 406d152cd6..7f91ceee68 100644
--- a/ide/coq_lex.mll
+++ b/ide/coq_lex.mll
@@ -86,7 +86,7 @@ let sentence_sep = '.' [ ' ' '\r' '\n' '\t' ]
 let multiword_declaration =
   "Module" (space+ "Type")?
 | "Program" space+ ident
-| "Existing" space+ "Instance"
+| "Existing" space+ "Instance" "s"?
 | "Canonical" space+ "Structure"
 
 let locality = ("Local" space+)?
-- 
cgit v1.2.3