X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FprimitiveTactics.ml;h=06e83a125335ea218df3a3e25f2c02f197910397;hb=b84c60ff48a21a62a08e636f32cf0df46dfbe45a;hp=3fefc662a5bcb7915e83ffb70bb9df4ea44a3bfd;hpb=25ec5b95fe67bbdee888a8268b3772a394cd74a5;p=helm.git

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index 3fefc662a..06e83a125 100644
--- 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)])