mquery.ml now really call the execution of the query.

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

diff --git a/helm/gTopLevel/mquery.mli b/helm/gTopLevel/mquery.mli
index d7889cb517694947c7b510af63309718bfcd93f2..bfdf89597e4c43cb910f46d7a2bd2fe83aa05284 100644 (file)
--- a/helm/gTopLevel/mquery.mli
+++ b/helm/gTopLevel/mquery.mli
@@ -43,3 +43,5 @@ val locate    : string -> string               (* LOCATE query building function
 
 val backward  : Cic.term -> string             (* BACKWARD query building function *)
 
+val init : unit -> unit
+val close : unit -> unit