name specifications added for elim_intros, elim_intros_simpl and elim_type

[helm.git] / helm / ocaml / tactics / eliminationTactics.mli

diff --git a/helm/ocaml/tactics/eliminationTactics.mli b/helm/ocaml/tactics/eliminationTactics.mli
index 92d9eee016ebdcbb2d941d4ee54614f69f651760..111bc57470eb826265fb3fde1992c9bf8216477a 100644 (file)
--- 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: