summaryrefslogtreecommitdiff
path: root/Util/VS2010/Dafny
diff options
context:
space:
mode:
authorGravatar Rustan Leino <leino@microsoft.com>2012-01-04 15:08:06 -0800
committerGravatar Rustan Leino <leino@microsoft.com>2012-01-04 15:08:06 -0800
commita48ad2338c6f4f162f89c50000d223a1b8a378b7 (patch)
tree702edd49679244a5a361b52a0ca3bf45f6c46df1 /Util/VS2010/Dafny
parentfeb840650169f8e89d752307e7c4d699281b1958 (diff)
Dafny: Start of new refinement features -- clean out old ones
Diffstat (limited to 'Util/VS2010/Dafny')
-rw-r--r--Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs4
1 files changed, 1 insertions, 3 deletions
diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
index f2924420..e35383b0 100644
--- a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
+++ b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
@@ -18,7 +18,7 @@ namespace Demo
this.MarkReservedWords( // NOTE: these keywords must also appear once more below
"class", "ghost", "static", "var", "method", "constructor", "datatype", "type",
- "assert", "assume", "new", "this", "object", "refines", "replaces", "by",
+ "assert", "assume", "new", "this", "object", "refines",
"unlimited", "module", "imports",
"if", "then", "else", "while", "invariant",
"break", "label", "return", "parallel", "havoc", "print",
@@ -274,8 +274,6 @@ namespace Demo
| "this"
| "object"
| "refines"
- | "replaces"
- | "by"
| "unlimited"
| "module"
| "imports"