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

diff --git a/helm/ocaml/tactics/eliminationTactics.mli b/helm/ocaml/tactics/eliminationTactics.mli
index 92d9eee01..cf6589f9a 100644
--- a/helm/ocaml/tactics/eliminationTactics.mli
+++ b/helm/ocaml/tactics/eliminationTactics.mli
@@ -23,12 +23,11 @@
  * 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:
- ?uris_choice_callback:
-  ((UriManager.uri * int * (UriManager.uri * Cic.term) list) list ->
-   (UriManager.uri * int * (UriManager.uri * Cic.term) list) list) ->
- Cic.term ->
-  ProofEngineTypes.tactic
+ ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
+ ?user_types:((UriManager.uri * int) list) ->
+ dbd:HMysql.dbd -> string -> ProofEngineTypes.tactic