Better handling of queries. Now both the locate and backward queries give

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

diff --git a/helm/gTopLevel/mQueryGenerator.mli b/helm/gTopLevel/mQueryGenerator.mli
index 69cbfeba55e6f39496703fc96b84fd9697877adc..694fdcf1248fb49034ad9588030397cf7da3d719 100644 (file)
--- a/helm/gTopLevel/mQueryGenerator.mli
+++ b/helm/gTopLevel/mQueryGenerator.mli
@@ -42,8 +42,9 @@ val init      : unit -> unit     (* INIT database 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 locate    : string -> MathQL.mqresult * string
+                                 (* LOCATE query building function *)
 
-val backward  : Cic.metasenv -> Cic.context -> Cic.term -> int -> string
+val backward  :
+ Cic.metasenv -> Cic.context -> Cic.term -> int -> MathQL.mqresult * string
                                  (* BACKWARD query building function *)