]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/grafite_engine/grafiteEngine.ml
More opcodes (badly) implemented.
[helm.git] / helm / software / components / grafite_engine / grafiteEngine.ml
index 6b34c687ccf38fcf13c168c67c3d786e066860d5..ad4ae40c6c6d2e7f040e9ed82ec892d37db01cc6 100644 (file)
@@ -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