Generator updated for new MathQL.ml

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

diff --git a/helm/gTopLevel/mQueryGenerator.mli b/helm/gTopLevel/mQueryGenerator.mli
index 2e4e59d5c0fc0f26b8b142c69fe537b6e43f3d51..68c2ea2570859d7600719949b161d04fc3e2e729 100644 (file)
--- a/helm/gTopLevel/mQueryGenerator.mli
+++ b/helm/gTopLevel/mQueryGenerator.mli
@@ -35,12 +35,6 @@
 
 exception Discard  
 
-type levels_spec = (string * bool * int) list
-
-val levels_of_term    : Cic.metasenv -> Cic.context -> Cic.term -> levels_spec
-
-val string_of_levels  : levels_spec -> string -> string
-
 val set_log_file      : string -> unit
 
 (* the callback function must return false iff the query must be skipped *)