The parser (the lexer indeed) now use the locate query to locate an object

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

diff --git a/helm/gTopLevel/mQueryGenerator.mli b/helm/gTopLevel/mQueryGenerator.mli
index a07019688f06e837ebacd465ce65cf72b6aae792..0282c3c8dacf71dac985810d17d4d5eb29145dd9 100644 (file)
--- a/helm/gTopLevel/mQueryGenerator.mli
+++ b/helm/gTopLevel/mQueryGenerator.mli
@@ -40,7 +40,8 @@ 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 *)