name specifications added for elim_intros, elim_intros_simpl and elim_type

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

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index 3fefc662a5bcb7915e83ffb70bb9df4ea44a3bfd..06e83a125335ea218df3a3e25f2c02f197910397 100644 (file)
--- a/helm/ocaml/tactics/primitiveTactics.ml
+++ b/helm/ocaml/tactics/primitiveTactics.ml
@@ -574,17 +574,19 @@ let elim_tac ~term =
   mk_tactic (elim_tac ~term)
 ;;
 
-let elim_intros_tac ~term =
- Tacticals.then_ ~start:(elim_tac ~term)
-  ~continuation:(intros_tac ())
+let elim_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) 
+                    ?depth ?using what =
+ Tacticals.then_ ~start:(elim_tac ~term:what)
+  ~continuation:(intros_tac ~mk_fresh_name_callback ?howmany:depth ())
 ;;
 
 (* The simplification is performed only on the conclusion *)
-let elim_intros_simpl_tac ~term =
- Tacticals.then_ ~start:(elim_tac ~term)
+let elim_intros_simpl_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
+                          ?depth ?using what =
+ Tacticals.then_ ~start:(elim_tac ~term:what)
   ~continuation:
    (Tacticals.thens
-     ~start:(intros_tac ())
+     ~start:(intros_tac ~mk_fresh_name_callback ?howmany:depth ())
      ~continuations:
        [ReductionTactics.simpl_tac
          ~pattern:(ProofEngineTypes.conclusion_pattern None)])