diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-06-11 14:24:51 -0700 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-06-11 14:24:51 -0700 |
| commit | 5c1a175715be5391e9ed2e10550be79f5b476220 (patch) | |
| tree | b0a8673cd938e8799b8fb2bfdb62107ada8479a5 /Util/VS2010 | |
| parent | f146b1cf761b57aa573dfb0c3a892b40aa8486e9 (diff) | |
Dafny: removed support for the old keyword "unlimited" (all functions are limited)
Diffstat (limited to 'Util/VS2010')
| -rw-r--r-- | Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs | 3 | ||||
| -rw-r--r-- | Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs | 1 |
2 files changed, 1 insertions, 3 deletions
diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs index 635115fb..4244e817 100644 --- a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs +++ b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs @@ -19,7 +19,7 @@ namespace Demo this.MarkReservedWords( // NOTE: these keywords must also appear once more below
"class", "ghost", "static", "var", "method", "constructor", "datatype", "codatatype", "type",
"assert", "assume", "new", "this", "object", "refines",
- "unlimited", "module", "imports",
+ "module", "imports",
"if", "then", "else", "while", "invariant",
"break", "label", "return", "parallel", "havoc", "print",
"returns", "requires", "ensures", "modifies", "reads", "decreases",
@@ -275,7 +275,6 @@ namespace Demo | "this"
| "object"
| "refines"
- | "unlimited"
| "module"
| "imports"
| "if"
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs index 48faa5ec..d621b1a9 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs +++ b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs @@ -288,7 +288,6 @@ namespace DafnyLanguage case "this":
case "true":
case "type":
- case "unlimited":
case "var":
case "while":
#endregion
|