moved "hint" from Command to Macro

[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 74a6a749eb245704364bb4b4f34bd3681fd1c87f..cb06a8edf6dc9d67f410fed7689a6bf6ad2e8230 100644 (file)
--- 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))])