]> matita.cs.unibo.it Git - helm.git/blobdiff - components/grafite_engine/grafiteEngine.ml
helm_registry: added the pair unmarshaller
[helm.git] / components / grafite_engine / grafiteEngine.ml
index 2d0d691f18d271a99e739a30984a28769432a275..4539029af26e1b6d276904701c2a414d81693cc7 100644 (file)
@@ -61,8 +61,8 @@ let tactic_of_ast ast =
   match ast with
   | GrafiteAst.Absurd (_, term) -> Tactics.absurd term
   | GrafiteAst.Apply (_, term) -> Tactics.apply term
-  | GrafiteAst.ApplyS (_, term) ->
-     Tactics.applyS ~term ~dbd:(LibraryDb.instance ())
+  | GrafiteAst.ApplyS (_, term, params) ->
+     Tactics.applyS ~term ~params ~dbd:(LibraryDb.instance ())
   | GrafiteAst.Assumption _ -> Tactics.assumption
   | GrafiteAst.Auto (_,params) ->
       AutoTactic.auto_tac ~params ~dbd:(LibraryDb.instance ())