Decompose now has a new parameter which is the callback to call to select the

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

diff --git a/helm/gTopLevel/proofEngine.mli b/helm/gTopLevel/proofEngine.mli
index 0263fd1e7c31e8e07fb5bc23335905fb051ba1cd..deb8483ac0348e7b3cc31ea85e858edb79b4968b 100644 (file)
--- a/helm/gTopLevel/proofEngine.mli
+++ b/helm/gTopLevel/proofEngine.mli
@@ -81,7 +81,11 @@ val generalize : Cic.term -> unit
 val absurd : Cic.term -> unit
 val contradiction : unit -> unit
 
-val decompose : Cic.term -> unit
+val decompose :
+ uris_choice_callback:
+  ((UriManager.uri * int * (UriManager.uri * Cic.term) list) list ->
+   (UriManager.uri * int * (UriManager.uri * Cic.term) list) list) ->
+ Cic.term -> unit
 
 (*
 val decide_equality : unit -> unit