X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FprimitiveTactics.ml;h=7bbdbf6b068ece8400f291b3fc459a115076ba8a;hb=9415c1b38c7927adab499ddd75f9a19d650a9acd;hp=8abb946c6686e27a64e9060b5089c5c35a69ce23;hpb=6a5752ce7b5d3fc6fea133b49cf7fd7a9e03deb4;p=helm.git

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index 8abb946c6..7bbdbf6b0 100644
--- a/helm/ocaml/tactics/primitiveTactics.ml
+++ b/helm/ocaml/tactics/primitiveTactics.ml
@@ -405,7 +405,7 @@ let intros_tac ?howmany ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_
  in
   mk_tactic (intros_tac ~mk_fresh_name_callback ())
   
-let cut_tac?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) ~term=
+let cut_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) term =
  let cut_tac
   ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
   term (proof, goal)
@@ -440,7 +440,7 @@ let cut_tac?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[
  in
   mk_tactic (cut_tac ~mk_fresh_name_callback term)
 
-let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name ~subst:[]) ~term=
+let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name ~subst:[]) term =
  let letin_tac
   ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
   term (proof, goal)