Bug fixed: the following happened.

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

diff --git a/helm/ocaml/tactics/tacticChaser.mli b/helm/ocaml/tactics/tacticChaser.mli
index 847dbc8b8942ee3e4a33492d8f62cd83c9590b67..e7e63954a7d667d629ae420d365f068e62f30bc4 100644 (file)
--- a/helm/ocaml/tactics/tacticChaser.mli
+++ b/helm/ocaml/tactics/tacticChaser.mli
@@ -25,9 +25,16 @@
 
 val matchConclusion : MQIConn.handle ->
   ?output_html:(string -> unit) ->
-    (* boolean value: true = in main position *)
-  choose_must:((MQGTypes.uri * bool) list list ->
-               (MQGTypes.uri * bool) list ->
-               (MQGTypes.uri * bool) list) ->
+  choose_must:(MQGTypes.r_obj list list ->
+               MQGTypes.r_obj list ->
+               MQGTypes.r_obj list) ->
   unit -> status: ProofEngineTypes.status -> string list
 
+
+(* TODO: OLD CODE TO BE REMOVED
+val searchTheorem : status: ProofEngineTypes.status -> ProofEngineTypes.proof * ProofEngineTypes.goal list
+*)
+
+val searchTheorems : MQIConn.handle -> status: ProofEngineTypes.status -> (ProofEngineTypes.proof * ProofEngineTypes.goal list) list
+
+