Signature and concrete syntax of fold fixed.

[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 67b5733d2a0644ef7376a6eff154af6810af2942..86c7185ecf1308d75e1f34707059c1cc77f3fc1f 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAstPp.ml
+++ b/helm/ocaml/cic_transformations/tacticAstPp.ml
@@ -82,8 +82,9 @@ let rec pp_tactic = function
   | ElimType (_, term) -> "elim type " ^ pp_term_ast term
   | Exact (_, term) -> "exact " ^ pp_term_ast term
   | Exists _ -> "exists"
-  | Fold (_, kind, pattern) ->
-      sprintf "fold %s %s" (pp_reduction_kind kind) (pp_pattern pattern)
+  | Fold (_, kind, term, pattern) ->
+      sprintf "fold %s %s %s" (pp_reduction_kind kind)
+       (pp_term_ast term) (pp_pattern pattern)
   | FwdSimpl (_, hyp, idents) -> 
       sprintf "fwd %s%s" hyp 
         (match idents with [] -> "" | idents -> " " ^ pp_idents idents)