*** empty log message ***

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

diff --git a/helm/gTopLevel/mquery.mli b/helm/gTopLevel/mquery.mli
index bfdf89597e4c43cb910f46d7a2bd2fe83aa05284..3ea31b8d214585ed73f15b32cc27d745fcb11153 100644 (file)
--- a/helm/gTopLevel/mquery.mli
+++ b/helm/gTopLevel/mquery.mli
@@ -39,9 +39,10 @@ val out_query : Mathql.mquery -> string        (* HTML representation of a query
 
 val tref_uref : Mathql.mquref -> Mathql.mqtref (* "tref of uref" conversion *)
 
-val locate    : string -> string               (* LOCATE query building function *)
+val init      : unit -> unit                   (* INIT database function *)
+
+val close     : unit -> unit                   (* CLOSE database function *)
 
-val backward  : Cic.term -> string             (* BACKWARD query building function *)
+val locate    : string -> string               (* LOCATE query building function *)
 
-val init : unit -> unit
-val close : unit -> unit
+val backward  : Cic.term -> int -> string      (* BACKWARD query building function *)