X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2FtacticAst2Box.ml;fp=helm%2Focaml%2Fcic_transformations%2FtacticAst2Box.ml;h=f0626c7724d3056b0e224a3cda39ecdb5c3195b9;hb=60033ee6d57f253ce1b90e3758a69b85d13f6a41;hp=0eb2fbde130bb5a50a84e48d0fc79a94b5ae1fa1;hpb=fc9cad6c109e279130501114000edcfb9621075b;p=helm.git

diff --git a/helm/ocaml/cic_transformations/tacticAst2Box.ml b/helm/ocaml/cic_transformations/tacticAst2Box.ml
index 0eb2fbde1..f0626c772 100644
--- a/helm/ocaml/cic_transformations/tacticAst2Box.ml
+++ b/helm/ocaml/cic_transformations/tacticAst2Box.ml
@@ -46,7 +46,13 @@ let rec count_tactic current_size tac =
     | Compare (_, term) -> countterm (current_size + 7) term
     | Constructor (_, n) -> current_size + 12
     | Contradiction _ -> current_size + 13
-    | Cut (_, term) -> countterm (current_size + 4) term
+    | Cut (_, ident, term) ->
+       let id_size =
+        match ident with
+           None -> 0
+         | Some id -> String.length id + 4
+       in
+        countterm (current_size + 4 + id_size) term
     | DecideEquality _ -> current_size + 15
     | Decompose (_, term) ->
        countterm (current_size + 11) term
@@ -131,9 +137,6 @@ and big_tactic2box = function
 		Box.indent(ast2astBox term)])
   | Constructor (_,n) -> Box.Text ([],"constructor " ^ string_of_int n)
   | Contradiction _ -> Box.Text([],"contradiction")
-  | Cut (_, term) -> 
-      Box.V([],[Box.Text([],"cut");
-		Box.indent(ast2astBox term)])
   | DecideEquality _ -> Box.Text([],"decide equality")
   | Decompose (_, term) ->
       Box.V([],[Box.Text([],"decompose");