X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Fmquery.mli;h=3ea31b8d214585ed73f15b32cc27d745fcb11153;hb=bea50d8a7fdf4063d8bf42d2983734190457e030;hp=bfdf89597e4c43cb910f46d7a2bd2fe83aa05284;hpb=c2ad6c9e76a929cca23276aa0e9dbbfdd1ca469b;p=helm.git

diff --git a/helm/gTopLevel/mquery.mli b/helm/gTopLevel/mquery.mli
index bfdf89597..3ea31b8d2 100644
--- 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 *)