Syntax change: change where what => change what where.

[helm.git] / matita / components / grafite_parser / grafiteParser.ml

diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml
index c1b059991db9e8b21093f531b2413ff4c802841a..4ce91508293241391d9d01c0e09a578266bfb2c4 100644 (file)
--- a/matita/components/grafite_parser/grafiteParser.ml
+++ b/matita/components/grafite_parser/grafiteParser.ml
@@ -128,7 +128,7 @@ EXTEND
   ];
   pattern_spec: [
     [ res = OPT [
-       SYMBOL "{";
+       "in" ;
        wanted_and_sps =
         [ "match" ; wanted = tactic_term ;
           sps = OPT [ "in"; sps = sequent_pattern_spec -> sps ] ->
@@ -136,7 +136,7 @@ EXTEND
         | sps = sequent_pattern_spec ->
            None,Some sps
         ];
-       SYMBOL "}" ->
+       SYMBOL ";" ->
          let wanted,hyp_paths,goal_path =
           match wanted_and_sps with
              wanted,None -> wanted, [], Some N.UserInput
@@ -202,7 +202,7 @@ EXTEND
         G.NMacro(loc,G.Screenshot (loc, fname))
     | IDENT "cases"; what = tactic_term ; where = pattern_spec ->
         G.NTactic(loc,[G.NCases (loc, what, where)])
-    | IDENT "change"; what = pattern_spec; "with"; with_what = tactic_term -> 
+    | IDENT "change";  "with"; with_what = tactic_term; what = pattern_spec -> 
         G.NTactic(loc,[G.NChange (loc, what, with_what)])
     | SYMBOL "-"; id = IDENT ->
         G.NTactic(loc,[G.NClear (loc, [id])])