From 6d5413dfe7cb3be64f7c014c891ac05553daeb02 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 21 Nov 2011 12:05:17 +0000 Subject: [PATCH] Syntax change: change where what => change what where. --- matita/components/grafite_parser/grafiteParser.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml index b616a824b..4ce915082 100644 --- a/matita/components/grafite_parser/grafiteParser.ml +++ b/matita/components/grafite_parser/grafiteParser.ml @@ -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])]) -- 2.39.2