embedded commands ast into tacticals ast

[helm.git] / helm / ocaml / cic_transformations / tacticAst2Box.ml

diff --git a/helm/ocaml/cic_transformations/tacticAst2Box.ml b/helm/ocaml/cic_transformations/tacticAst2Box.ml
index 5d8fae1b6f463961d2610e80199602172ad158c0..4b79607f52b0384951baba7fe9921c00c8ed0967 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAst2Box.ml
+++ b/helm/ocaml/cic_transformations/tacticAst2Box.ml
@@ -227,7 +227,12 @@ and big_tactic2box ?(attr = []) = function
 open TacticAst
 
 let rec tactical2box ?(attr = []) = function
-    LocatedTactical (loc, tac) -> tactical2box tac
+  | LocatedTactical (loc, tac) -> tactical2box tac
+
+  | Tactic tac -> tactic2box tac
+  | Command cmd -> (* TODO dummy implementation *)
+      Box.Text([], TacticAstPp.pp_tactical (Command cmd))
+
   | Fail -> Box.Text([],"fail")
   | Do (count, tac) -> 
       Box.V([],[Box.Text([],"do " ^ string_of_int count);
@@ -238,7 +243,6 @@ let rec tactical2box ?(attr = []) = function
                Box.indent (tactical2box tac)])
   | Seq tacs -> 
       Box.V([],tacticals2box tacs)
-  | Tactic tac -> tactic2box tac
   | Then (tac, tacs) -> 
       Box.V([],[tactical2box tac;
                Box.H([],[Box.skip;