ocaml 3.09 transition

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

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