diff options
| author | herbelin | 2004-11-17 12:48:10 +0000 |
|---|---|---|
| committer | herbelin | 2004-11-17 12:48:10 +0000 |
| commit | ef638507c545a80b086f6757c4b2dbf1ed603219 (patch) | |
| tree | 1ad24a3c23c144921f5f6e29d2f367457448b3ae | |
| parent | f511a34d6de3b5be9b6a165dbd44b2dcfc8b6059 (diff) | |
Déclaration de '..' comme mot-clé (résoud bug #856)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6316 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | parsing/g_constr.ml4 | 2 | ||||
| -rw-r--r-- | parsing/g_constrnew.ml4 | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 02eda021ab..6f9a11f455 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -23,7 +23,7 @@ let constr_kw = ":"; "("; ")"; "["; "]"; "{"; "}"; ","; ";"; "->"; "="; ":="; "!"; "::"; "<:"; ":<"; "=>"; "<"; ">"; "|"; "?"; "/"; "<->"; "\\/"; "/\\"; "`"; "``"; "&"; "*"; "+"; "@"; "^"; "#"; "-"; - "~"; "'"; "<<"; ">>"; "<>" + "~"; "'"; "<<"; ">>"; "<>"; ".." ] let _ = if !Options.v7 then diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4 index 61cff830d0..60299ae8d5 100644 --- a/parsing/g_constrnew.ml4 +++ b/parsing/g_constrnew.ml4 @@ -22,7 +22,7 @@ open Util let constr_kw = [ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "in"; "for"; "end"; "as"; "let"; "if"; "then"; "else"; "return"; - "Prop"; "Set"; "Type"; ".("; "_" ] + "Prop"; "Set"; "Type"; ".("; "_"; ".." ] let _ = if not !Options.v7 then |