let reduce_tac ~pattern =
mk_tactic (reduction_tac ~reduction:ProofEngineReduction.reduce ~pattern);;
-let unfold_tac ?what ~pattern =
+let unfold_tac what ~pattern =
mk_tactic (reduction_tac ~reduction:(ProofEngineReduction.unfold ?what)
~pattern);;