A few other tactics made available to matita.

[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 f0626c7724d3056b0e224a3cda39ecdb5c3195b9..ba14fd0d635372a4480f3e9e7daa4af681e14ecf 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAst2Box.ml
+++ b/helm/ocaml/cic_transformations/tacticAst2Box.ml
@@ -65,8 +65,6 @@ let rec count_tactic current_size tac =
     | ElimType (_, term) -> countterm (current_size + 10) term
     | Exact (_, term) -> countterm (current_size + 6) term
     | Exists _ -> current_size + 6
-    | Fold (_, kind, term) ->
-       countterm (current_size + 5) term
     | Fourier _ -> current_size + 7
     | Goal (_, n) -> current_size + 4 + int_of_float (ceil (log10 (float n)))
     | Injection (_, term) ->
@@ -79,9 +77,6 @@ let rec count_tactic current_size tac =
     | LetIn (_, term, ident) ->
        countterm (current_size + 5 + String.length ident) term
     | Reflexivity _ -> current_size + 11
-    | Replace (_, t1, t2) -> 
-       let size1 = countterm (current_size + 14) t1 in (* replace, with *)
-         countterm size1 t2    
     | Right _ -> current_size + 5
     | Ring _ -> current_size + 4
     | Split _ -> current_size + 5
@@ -162,11 +157,6 @@ and big_tactic2box = function
       Box.V([],[Box.Text([],"exact");
                Box.indent(ast2astBox term)])
   | Exists _ -> Box.Text([],"exists")
-  | Fold (_, kind, term) ->
-      Box.V([],[Box.H([],[Box.Text([],"fold");
-                         Box.smallskip;
-                         Box.Text([],string_of_kind kind)]);
-               Box.indent(ast2astBox term)])
   | Fourier _ -> Box.Text([],"fourier")
   | Goal (_, n) -> Box.Text([],"goal " ^ string_of_int n)
   | Intros (_, num, idents) ->
@@ -188,14 +178,6 @@ and big_tactic2box = function
                          Box.Text([],"=")]);
                Box.indent (ast2astBox term)])
   | Reflexivity _ -> Box.Text([],"reflexivity")
-  | Replace (_, t1, t2) -> 
-      Box.V([],
-           (pretty_append 
-              [Box.Text([],"replace")]
-              t1)@
-           (pretty_append 
-              [Box.Text([],"with")]
-              t2))
   | Right _ -> Box.Text([],"right")
   | Ring _ ->  Box.Text([],"ring")
   | Split _ -> Box.Text([],"split")
@@ -209,16 +191,9 @@ open TacticAst
 
 let rec tactical2box = function
   | 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);
                Box.indent (tactical2box tac)])
-  | IdTac _ -> Box.Text([],"id")
   | Repeat (_, tac) -> 
       Box.V([],[Box.Text([],"repeat");
                Box.indent (tactical2box tac)])