diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-06 11:38:31 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-06 11:38:31 +0000 |
| commit | 7a7a09378e492b5b2dc87e3a8e502e842ca1faf5 (patch) | |
| tree | 3a71b586ed39ea4c81eb12c81044ae8007c8d57a /ide/coq_lex.mll | |
| parent | f8e8ffa4b7c42f6c53126d284c0bfbf8a992bc89 (diff) | |
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
Diffstat (limited to 'ide/coq_lex.mll')
| -rw-r--r-- | ide/coq_lex.mll | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/coq_lex.mll b/ide/coq_lex.mll index 406d152cd..7f91ceee6 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+)? |