...

[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 bbb2c935b7e8233f47a4f214ad22dcc441ae244e..019ba6172a2c413c777f737f4250c57475f8afd6 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAstPp.ml
+++ b/helm/ocaml/cic_transformations/tacticAstPp.ml
@@ -85,8 +85,10 @@ 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)
+  | Generalize (_, term, ident, pattern) ->
+     sprintf "generalize %s%s %s" (pp_term_ast term)
+      (match ident with None -> "" | Some id -> " as " ^ id)
+      (pp_pattern pattern)
   | Goal (_, n) -> "goal " ^ string_of_int n
   | Fourier _ -> "fourier"
   | Injection (_, term) -> "injection " ^ pp_term_ast term