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 3c4026f95137deba0ecb6da57323c2cfd5f43770..4b79607f52b0384951baba7fe9921c00c8ed0967 100644 (file)
--- 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;