]> matita.cs.unibo.it Git - helm.git/commitdiff
Syntax change: change where what => change what where.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 21 Nov 2011 12:05:17 +0000 (12:05 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 21 Nov 2011 12:05:17 +0000 (12:05 +0000)
matita/components/grafite_parser/grafiteParser.ml

index b616a824b2d8c547a80cce9ae440ed9b114be7e3..4ce91508293241391d9d01c0e09a578266bfb2c4 100644 (file)
@@ -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])])