X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FtacticChaser.mli;h=d4f8a2c540402273b79173416dfab3439b186cc8;hb=a6fc115fd7d4cfba94a43f001f4c27322d3db1a8;hp=e7e63954a7d667d629ae420d365f068e62f30bc4;hpb=f654787b2156ede958a1d35ca8daf239de1b7b89;p=helm.git

diff --git a/helm/ocaml/tactics/tacticChaser.mli b/helm/ocaml/tactics/tacticChaser.mli
index e7e63954a..d4f8a2c54 100644
--- a/helm/ocaml/tactics/tacticChaser.mli
+++ b/helm/ocaml/tactics/tacticChaser.mli
@@ -28,13 +28,14 @@ val matchConclusion : MQIConn.handle ->
   choose_must:(MQGTypes.r_obj list list ->
                MQGTypes.r_obj list ->
                MQGTypes.r_obj list) ->
-  unit -> status: ProofEngineTypes.status -> string list
+  unit -> ProofEngineTypes.status -> string list
 
 
 (* TODO: OLD CODE TO BE REMOVED
-val searchTheorem : status: ProofEngineTypes.status -> ProofEngineTypes.proof * ProofEngineTypes.goal list
+val searchTheorem : ProofEngineTypes.status -> ProofEngineTypes.proof * ProofEngineTypes.goal list
 *)
 
-val searchTheorems : MQIConn.handle -> status: ProofEngineTypes.status -> (ProofEngineTypes.proof * ProofEngineTypes.goal list) list
-
+val searchTheorems:
+  MQIConn.handle -> ProofEngineTypes.status ->
+    (ProofEngineTypes.proof * ProofEngineTypes.goal list) list