X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2FtacticAst2Box.ml;h=cb06a8edf6dc9d67f410fed7689a6bf6ad2e8230;hb=aca103d3c3d740efcc0bcc2932922cff77facb49;hp=74a6a749eb245704364bb4b4f34bd3681fd1c87f;hpb=0575a1cb077087970f311b48f2e45dc4a01a6867;p=helm.git

diff --git a/helm/ocaml/cic_transformations/tacticAst2Box.ml b/helm/ocaml/cic_transformations/tacticAst2Box.ml
index 74a6a749e..cb06a8edf 100644
--- a/helm/ocaml/cic_transformations/tacticAst2Box.ml
+++ b/helm/ocaml/cic_transformations/tacticAst2Box.ml
@@ -69,7 +69,6 @@ let rec count_tactic current_size tac =
 	countterm (current_size + 5) term
     | Fourier _ -> current_size + 7
     | Goal (_, n) -> current_size + 4 + int_of_float (ceil (log10 (float n)))
-    | Hint _ -> current_size + 4
     | Injection (_, ident) -> current_size + 10 + (String.length ident)
     | Intros (_, num, idents) ->
 	List.fold_left 
@@ -191,7 +190,6 @@ and big_tactic2box = function
 		Box.indent(ast2astBox term)])
   | Fourier _ -> Box.Text([],"fourier")
   | Goal (_, n) -> Box.Text([],"goal " ^ string_of_int n)
-  | Hint _ -> Box.Text([],"hint")
   | Injection (_, ident) -> 
       Box.V([],[Box.Text([],"transitivity");
 		Box.indent (Box.Text([],ident))])