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

diff --git a/helm/ocaml/cic_transformations/tacticAst2Box.ml b/helm/ocaml/cic_transformations/tacticAst2Box.ml
index 3c4026f95..4b79607f5 100644
--- a/helm/ocaml/cic_transformations/tacticAst2Box.ml
+++ b/helm/ocaml/cic_transformations/tacticAst2Box.ml
@@ -93,7 +93,7 @@ let rec count_tactic current_size tac =
 
 let is_big_tac tac =
   let n = (count_tactic 0 tac) in
-  prerr_endline ("Lunghezza: " ^ (string_of_int n));
+(*   prerr_endline ("Lunghezza: " ^ (string_of_int n)); *)
   n > maxsize
 ;;
 
@@ -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;