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)
=