Decompose now has a new parameter that is the callback function to call

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

diff --git a/helm/ocaml/tactics/eliminationTactics.mli b/helm/ocaml/tactics/eliminationTactics.mli
index a49c771585dee99989e0a910f64869c18b742d28..5e132c4966366860cad1e3cefa44b881e7aa1c2b 100644 (file)
--- a/helm/ocaml/tactics/eliminationTactics.mli
+++ b/helm/ocaml/tactics/eliminationTactics.mli
@@ -25,9 +25,9 @@
 
 val elim_type_tac: term:Cic.term -> ProofEngineTypes.tactic
 
-val interactive_user_uri_choice: ( selection_mode:[`SINGLE | `EXTENDED] ->
-      ?ok:string ->
-      ?enable_button_for_non_vars:bool ->
-      title:string -> msg:string -> string list -> string list) ref
-
-val decompose_tac: term:Cic.term -> ProofEngineTypes.tactic
+val decompose_tac:
+ term:Cic.term ->
+ uris_choice_callback:
+  ((UriManager.uri * int * (UriManager.uri * Cic.term) list) list ->
+   (UriManager.uri * int * (UriManager.uri * Cic.term) list) list) ->
+   ProofEngineTypes.tactic