X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2FtacticAst2Box.ml;h=4b79607f52b0384951baba7fe9921c00c8ed0967;hb=0c6a5aadb1a7746681a8e26fc0b009f847c10557;hp=5d8fae1b6f463961d2610e80199602172ad158c0;hpb=ed3cc138a0066b654db61f28a176c54d35a4ddc3;p=helm.git

diff --git a/helm/ocaml/cic_transformations/tacticAst2Box.ml b/helm/ocaml/cic_transformations/tacticAst2Box.ml
index 5d8fae1b6..4b79607f5 100644
--- 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;