New argument (the hypothesis name) for cut.

[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 0eb2fbde130bb5a50a84e48d0fc79a94b5ae1fa1..f0626c7724d3056b0e224a3cda39ecdb5c3195b9 100644 (file)
--- 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");