Renamed "parallel" statement to "forall" statement, and made the parentheses around the bound variables optional.

4 files changed, 5 insertions, 6 deletions

diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el
index d1bdcf12..b043150c 100644
--- a/Util/Emacs/dafny-mode.el
+++ b/Util/Emacs/dafny-mode.el
@@ -40,7 +40,7 @@
    `(,(dafny-regexp-opt '(

         "assert" "assume" "break" "choose" "then" "else" "if" "label" "return" "yield"

         "while" "print" "where"

-        "old" "forall" "exists" "new" "parallel" "calc" "in" "this" "fresh"

+        "old" "forall" "exists" "new" "calc" "in" "this" "fresh"

         "match" "case" "false" "true" "null")) . font-lock-keyword-face)

    `(,(dafny-regexp-opt '("array" "array2" "array3" "bool" "multiset" "map" "nat" "int" "object" "set" "seq")) . font-lock-type-face)

    )

diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
index dd910820..fe7c6638 100644
--- a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
+++ b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
@@ -22,7 +22,7 @@ namespace Demo
           "assert", "assume", "new", "this", "object", "refines",

           "abstract", "module", "import", "as", "default", "opened",

           "if", "then", "else", "while", "invariant",

-          "break", "label", "return", "yield", "parallel", "print",

+          "break", "label", "return", "yield", "print",

           "returns", "yields", "requires", "ensures", "modifies", "reads", "decreases",

           "bool", "nat", "int", "false", "true", "null",

           "function", "predicate", "copredicate", "free",

@@ -293,7 +293,6 @@ namespace Demo
           | "label"

           | "return"

           | "yield"

-          | "parallel"

           | "calc"

           | "print"

           | "returns"

diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty
index 4a3f6dbc..e3007b75 100644
--- a/Util/latex/dafny.sty
+++ b/Util/latex/dafny.sty
@@ -16,12 +16,13 @@
       match,case,false,true,null,old,fresh,choose,this,

       % statements

       assert,assume,print,new,if,then,else,while,invariant,break,label,return,yield,

-      parallel,where,calc

+      where,calc

       },

   literate=%

     {:}{$\colon$}1

     {::}{$\bullet$}2

     {:=}{$:$$=$}2

+    {:|}{${:}\!\!|$}2

     {!}{$\lnot$}1

     {!!}{$\not\cap$}1

     {==}{$=$}1

@@ -31,7 +32,6 @@
     {<=}{$\le$}1

     {>=}{$\ge$}1

     % the following isn't actually Dafny, but it gives the option to produce nicer latex

-    {|=>}{$\Rightarrow$}2

     {<=set}{$\subseteq$}1

     {+set}{$\cup$}1

     {*set}{$\cap$}1

diff --git a/Util/vim/dafny.vim b/Util/vim/dafny.vim
index b329f0f7..31f27c51 100644
--- a/Util/vim/dafny.vim
+++ b/Util/vim/dafny.vim
@@ -10,7 +10,7 @@ syntax keyword method constructor comethod
 syntax keyword dafnyTypeDef class datatype codatatype type iterator
 syntax keyword abstract module import opened as default
 syntax keyword dafnyConditional if then else match case 
-syntax keyword dafnyRepeat while parallel
+syntax keyword dafnyRepeat while
 syntax keyword dafnyStatement assume assert return yield new print break label where calc
 syntax keyword dafnyKeyword var ghost returns yields null static this refines
 syntax keyword dafnyType bool nat int seq set multiset object array array2 array3 map