(* *)
(******************************************************************************)
-val levels : Cic.metasenv -> Cic.context -> Cic.term -> int -> string
+val levels : Cic.metasenv -> Cic.context -> Cic.term -> string
(* level assignment testing function *)
+val call_back : (MathQL.mquery -> bool) -> unit
+
val init : unit -> unit (* INIT database function *)
val close : unit -> unit (* CLOSE database function *)
-val locate : string -> string (* LOCATE query building 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 *)