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)
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)