X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FprimitiveTactics.ml;h=fa696856010431f53bb14546df11163a440c61b0;hb=03cb4be465e546a00f870213b14dcf1b71c4831d;hp=c411340ae829ee94159f7ac90e5d0e76c7882a71;hpb=59a077151336a0e73804572b52fb757a0e7f6a97;p=helm.git

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index c411340ae..fa6968560 100644
--- a/helm/ocaml/tactics/primitiveTactics.ml
+++ b/helm/ocaml/tactics/primitiveTactics.ml
@@ -382,7 +382,7 @@ let intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name) ()=
  in
   mk_tactic (intros_tac ~mk_fresh_name_callback ())
   
-let cut_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name) term=
+let cut_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name) ~term=
  let cut_tac
   ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name)
   term (proof, goal)
@@ -417,7 +417,7 @@ let cut_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name) term=
  in
   mk_tactic (cut_tac ~mk_fresh_name_callback term)
 
-let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name) term=
+let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name) ~term=
  let letin_tac
   ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name)
   term (proof, goal)