X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FreductionTactics.ml;h=f5c82a9fe7da0be3f2702d90c5733a99cc3c6f4d;hb=91a095f0686ee569ba035e4e30c7d071588cb8e7;hp=492b265cb5b3e97e0a26077b402104bb673430e5;hpb=6d93d688ae2da401417f64ffd5ee6ffccaa89fc1;p=helm.git

diff --git a/helm/ocaml/tactics/reductionTactics.ml b/helm/ocaml/tactics/reductionTactics.ml
index 492b265cb..f5c82a9fe 100644
--- 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);;