X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FmQueryGenerator.mli;h=69cbfeba55e6f39496703fc96b84fd9697877adc;hb=1d4de3a17c0a41781cc8e415361d228ded4f1d8f;hp=2d07f4ec491d82b196f421972e4b06bd0fdd9531;hpb=ec899ba2461af8c3f0ef253a8879fc1882b8b46f;p=helm.git

diff --git a/helm/gTopLevel/mQueryGenerator.mli b/helm/gTopLevel/mQueryGenerator.mli
index 2d07f4ec4..69cbfeba5 100644
--- a/helm/gTopLevel/mQueryGenerator.mli
+++ b/helm/gTopLevel/mQueryGenerator.mli
@@ -33,10 +33,17 @@
 (*                                                                            *)
 (******************************************************************************)
 
-val init      : unit -> unit                   (* INIT database function *)
+val levels    : Cic.metasenv -> Cic.context -> Cic.term -> string
+                                 (* level assignment testing function *)
 
-val close     : unit -> unit                   (* CLOSE database function *)
+val call_back : (MathQL.mquery -> bool) -> unit
 
-val locate    : string -> string               (* LOCATE query building function *)
+val init      : unit -> unit     (* INIT database function *)
 
-val backward  : Cic.term -> int -> string      (* BACKWARD query building function *)
+val close     : unit -> unit     (* CLOSE database function *)
+
+val locate    : string -> MathQL.mqresult (* LOCATE query building function *)
+val locate_html : string -> string (* LOCATE query building function *)
+
+val backward  : Cic.metasenv -> Cic.context -> Cic.term -> int -> string
+                                 (* BACKWARD query building function *)