From d47400c8a1ba72497cc145173aa6ad9f6b1b5a85 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Sun, 23 Feb 2014 17:27:26 -0800 Subject: Deprecated "comethod" keyword in favor of "colemma". (Also, "prefix method" -> "prefix lemma") --- Util/Emacs/dafny-mode.el | 2 +- Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs | 4 ++-- Util/latex/dafny.sty | 2 +- Util/vim/dafny.vim | 2 +- 4 files changed, 5 insertions(+), 5 deletions(-) (limited to 'Util') diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el index c77fed74..d663665b 100644 --- a/Util/Emacs/dafny-mode.el +++ b/Util/Emacs/dafny-mode.el @@ -32,7 +32,7 @@ `(,(dafny-regexp-opt '( "class" "datatype" "codatatype" "type" "iterator" "function" "predicate" "copredicate" - "ghost" "var" "method" "lemma" "constructor" "comethod" "colemma" + "ghost" "var" "method" "lemma" "constructor" "colemma" "abstract" "module" "import" "default" "as" "opened" "static" "refines" "returns" "yields" "requires" "ensures" "modifies" "reads" "free" "invariant" "decreases" "include" diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs index fe7c6638..d8ec579a 100644 --- a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs +++ b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs @@ -17,7 +17,7 @@ namespace Demo StringLiteral stringLiteral = TerminalFactory.CreateCSharpString("String"); this.MarkReservedWords( // NOTE: these keywords must also appear once more below - "class", "ghost", "static", "var", "method", "constructor", "comethod", "datatype", "codatatype", + "class", "ghost", "static", "var", "method", "constructor", "colemma", "datatype", "codatatype", "iterator", "type", "assert", "assume", "new", "this", "object", "refines", "abstract", "module", "import", "as", "default", "opened", @@ -267,7 +267,7 @@ namespace Demo | "var" | "method" | "constructor" - | "comethod" + | "colemma" | "datatype" | "codatatype" | "type" diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty index d4624def..41e0779b 100644 --- a/Util/latex/dafny.sty +++ b/Util/latex/dafny.sty @@ -9,7 +9,7 @@ bool,nat,int,real,object,set,multiset,seq,array,array2,array3,map, function,predicate,copredicate, ghost,var,static,refines, - method,lemma,constructor,comethod,colemma, + method,lemma,constructor,colemma, returns,yields,abstract,module,import,default,opened,as,in, requires,modifies,ensures,reads,decreases,free,include % expressions diff --git a/Util/vim/dafny.vim b/Util/vim/dafny.vim index 06e1252e..f533a621 100644 --- a/Util/vim/dafny.vim +++ b/Util/vim/dafny.vim @@ -6,7 +6,7 @@ syntax clear syntax case match syntax keyword dafnyFunction function predicate copredicate -syntax keyword method lemma constructor comethod colemma +syntax keyword method lemma constructor colemma syntax keyword dafnyTypeDef class datatype codatatype type iterator syntax keyword abstract module import opened as default syntax keyword dafnyConditional if then else match case -- cgit v1.2.3