Tactic generalize ported to patterns and activated in 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 902a1d661eeabda075b9e8c1cc760b97610625f0..35a27ff24785fa17640b023ebc5d374efd95a076 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAst2Box.ml
+++ b/helm/ocaml/cic_transformations/tacticAst2Box.ml
@@ -68,6 +68,7 @@ let rec count_tactic current_size tac =
     | Fold (_, kind, term) ->
        countterm (current_size + 5) term
     | Fourier _ -> current_size + 7
+    | Generalize (_,term,pattern) -> assert false (* TODO *)
     | Goal (_, n) -> current_size + 4 + int_of_float (ceil (log10 (float n)))
     | Injection (_, ident) -> current_size + 10 + (String.length ident)
     | Intros (_, num, idents) ->
@@ -191,6 +192,7 @@ and big_tactic2box = function
                          Box.Text([],string_of_kind kind)]);
                Box.indent(ast2astBox term)])
   | Fourier _ -> Box.Text([],"fourier")
+  | Generalize _ -> assert false  (* TODO *)
   | Goal (_, n) -> Box.Text([],"goal " ^ string_of_int n)
   | Injection (_, ident) -> 
       Box.V([],[Box.Text([],"transitivity");