mQueryGenerator and topLevel patched

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

diff --git a/helm/gTopLevel/mQueryGenerator.mli b/helm/gTopLevel/mQueryGenerator.mli
index 0282c3c8dacf71dac985810d17d4d5eb29145dd9..69cbfeba55e6f39496703fc96b84fd9697877adc 100644 (file)
--- a/helm/gTopLevel/mQueryGenerator.mli
+++ b/helm/gTopLevel/mQueryGenerator.mli
@@ -33,9 +33,11 @@
 (*                                                                            *)
 (******************************************************************************)
 
-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 *)