Signature and concrete syntax of fold fixed.

[helm.git] / helm / ocaml / tactics / reductionTactics.ml

diff --git a/helm/ocaml/tactics/reductionTactics.ml b/helm/ocaml/tactics/reductionTactics.ml
index ae99ecb33d486be1f0069a9fce4b46f076b3a5f5..18db1a302dab0a3cbec4849e32202ca0bc137b27 100644 (file)
--- a/helm/ocaml/tactics/reductionTactics.ml
+++ b/helm/ocaml/tactics/reductionTactics.ml
@@ -83,7 +83,7 @@ let whd_tac ~pattern =
 let normalize_tac ~pattern = 
  mk_tactic (reduction_tac ~reduction:CicReduction.normalize ~pattern );;
 
-let fold_tac ~reduction ~pattern =
+let fold_tac ~reduction ~term ~pattern =
 (*
  let fold_tac ~reduction ~pattern:(hyp_patterns,goal_pattern) ~term (proof,goal)
  =