Added Decompose tactic

[helm.git] / helm / gTopLevel / eliminationTactics.mli

diff --git a/helm/gTopLevel/eliminationTactics.mli b/helm/gTopLevel/eliminationTactics.mli
index 00ccedd64efe99bbed7a4e4389ca43c8973675b5..a49c771585dee99989e0a910f64869c18b742d28 100644 (file)
--- a/helm/gTopLevel/eliminationTactics.mli
+++ b/helm/gTopLevel/eliminationTactics.mli
@@ -25,4 +25,9 @@
 
 val elim_type_tac: term:Cic.term -> ProofEngineTypes.tactic
 
-val decompose_tac: clist:(Cic.term list) -> 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