Tactic generalize ported to patterns and activated in matita.

[helm.git] / helm / ocaml / cic_transformations / tacticAstPp.ml

diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml
index 2cc4d0c658fc735306b45b6ebbed2a86c210f18c..86d10c87730294bf0db4e097c4ec442dec47f3e4 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAstPp.ml
+++ b/helm/ocaml/cic_transformations/tacticAstPp.ml
@@ -80,6 +80,8 @@ let rec pp_tactic = function
   | Exists _ -> "exists"
   | Fold (_, kind, term) ->
       sprintf "fold %s %s" (pp_reduction_kind kind) (pp_term_ast term)
+  | Generalize (_, term, pattern) ->
+     sprintf "generalize %s %s" (pp_term_ast term) (pp_pattern pattern)
   | Goal (_, n) -> "goal " ^ string_of_int n
   | Fourier _ -> "fourier"
   | Injection (_, ident) -> "injection " ^ ident