1. ProofEngineHelpers.locate_in_term, ProofEngineHelpers.locate_in_conjecture

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

diff --git a/helm/ocaml/tactics/reductionTactics.ml b/helm/ocaml/tactics/reductionTactics.ml
index 492b265cb5b3e97e0a26077b402104bb673430e5..f5c82a9fe7da0be3f2702d90c5733a99cc3c6f4d 100644 (file)
--- a/helm/ocaml/tactics/reductionTactics.ml
+++ b/helm/ocaml/tactics/reductionTactics.ml
@@ -79,7 +79,7 @@ let simpl_tac ~pattern =
 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);;