generate dot files with attributes on nodes (instead of only edges), and added genera...

[helm.git] / helm / software / components / grafite_engine / grafiteEngine.ml

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index ebe7df36977901b7b8351f3af62db67f45a30306..ab43c6cc18e67c0684562e4ed2a6dffeacb589bf 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -154,6 +154,13 @@ let tactic_of_ast ast =
   | GrafiteAst.Split _ -> Tactics.split
   | GrafiteAst.Symmetry _ -> Tactics.symmetry
   | GrafiteAst.Transitivity (_, term) -> Tactics.transitivity term
+  (* Implementazioni Aggiunte *)
+  | GrafiteAst.Assume (_, id, t) -> Declarative.assume id t
+  | GrafiteAst.Suppose (_, t, id) -> Declarative.suppose t id
+  | GrafiteAst.By_term_we_proved (_, t, ty, id) ->
+     Declarative.by_term_we_proved t ty id
+  | GrafiteAst.We_need_to_prove (_, t, id) -> Declarative.we_need_to_prove t id
+  | GrafiteAst.Bydone (_, t) -> Declarative.bydone t
 
 (* maybe we only need special cases for apply and goal *)
 let classify_tactic tactic =