X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=ad4ae40c6c6d2e7f040e9ed82ec892d37db01cc6;hb=82d0bc4291648c88e9f248fc5a67518e938eacdf;hp=6b34c687ccf38fcf13c168c67c3d786e066860d5;hpb=3990759a81db3ce45bf4ec56e1985e532151f6e0;p=helm.git

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 6b34c687c..ad4ae40c6 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -96,8 +96,8 @@ let rec tactic_of_ast status ast =
      Tactics.change ~pattern with_what
   | GrafiteAst.Clear (_,id) -> Tactics.clear id
   | GrafiteAst.ClearBody (_,id) -> Tactics.clearbody id
-  | GrafiteAst.Compose (_,t1,t2,(howmany, names)) -> 
-      Tactics.compose t1 t2 ?howmany
+  | GrafiteAst.Compose (_,t1,t2,times,(howmany, names)) -> 
+      Tactics.compose times t1 t2 ?howmany
         ~mk_fresh_name_callback:(namer_of names)
   | GrafiteAst.Contradiction _ -> Tactics.contradiction
   | GrafiteAst.Constructor (_, n) -> Tactics.constructor n