X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FeliminationTactics.mli;h=111bc57470eb826265fb3fde1992c9bf8216477a;hb=7033b0a141f65fd75b435a6f71325ca67f19db61;hp=92d9eee016ebdcbb2d941d4ee54614f69f651760;hpb=bac72fcaa876137ab7a5630e0c1badc2a627dce8;p=helm.git

diff --git a/helm/ocaml/tactics/eliminationTactics.mli b/helm/ocaml/tactics/eliminationTactics.mli
index 92d9eee01..111bc5747 100644
--- a/helm/ocaml/tactics/eliminationTactics.mli
+++ b/helm/ocaml/tactics/eliminationTactics.mli
@@ -23,7 +23,9 @@
  * http://cs.unibo.it/helm/.
  *)
 
-val elim_type_tac: term:Cic.term -> ProofEngineTypes.tactic
+val elim_type_tac: 
+  ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
+  ?depth:int -> ?using:Cic.term -> Cic.term -> ProofEngineTypes.tactic
 
 (* The default callback always decomposes the term as much as possible *)
 val decompose_tac: