(* *)
(******************************************************************************)
-val init : unit -> unit (* INIT database function *)
+val levels : Cic.metasenv -> Cic.context -> Cic.term -> int -> string
+ (* level assignment testing function *)
-val close : unit -> unit (* CLOSE database function *)
+val init : unit -> unit (* INIT database function *)
-val locate : string -> string (* LOCATE query building function *)
+val close : unit -> unit (* CLOSE database function *)
-val backward : Cic.term -> int -> string (* BACKWARD query building function *)
+val locate : string -> string (* LOCATE query building function *)
+
+val backward : Cic.metasenv -> Cic.context -> Cic.term -> int -> string
+ (* BACKWARD query building function *)