new more flexible compose, see matita/tests/compose.ma for a sample

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

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index 10a841e2eae14e01db81a03147ca3ace7ebb8bfe..45a71f174dea678322b79bd97fcaecf0e5a31b79 100644 (file)
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -156,9 +156,10 @@ EXTEND
         GrafiteAst.ClearBody (loc,id)
     | IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
         GrafiteAst.Change (loc, what, t)
-    | IDENT "compose"; t1 = tactic_term; t2 = tactic_term;
-      specs = intros_spec ->
-        GrafiteAst.Compose (loc, t1, t2, specs)
+    | IDENT "compose"; times = OPT int; t1 = tactic_term; t2 = 
+      OPT [ "with"; t = tactic_term -> t ]; specs = intros_spec ->
+        let times = match times with None -> 1 | Some i -> i in
+        GrafiteAst.Compose (loc, t1, t2, times, specs)
     | IDENT "constructor"; n = int ->
         GrafiteAst.Constructor (loc, n)
     | IDENT "contradiction" ->