X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FeliminationTactics.mli;h=cf6589f9a5bb3c83c9d6d6d5f6718ff7e2332b8b;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=111bc57470eb826265fb3fde1992c9bf8216477a;hpb=249d79bebff886846fbab65cc079623d90684baf;p=helm.git

diff --git a/helm/ocaml/tactics/eliminationTactics.mli b/helm/ocaml/tactics/eliminationTactics.mli
index 111bc5747..cf6589f9a 100644
--- a/helm/ocaml/tactics/eliminationTactics.mli
+++ b/helm/ocaml/tactics/eliminationTactics.mli
@@ -27,10 +27,7 @@ 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