- added and exposed get_current_status_as_xml

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

diff --git a/helm/gTopLevel/mQueryLevels.mli b/helm/gTopLevel/mQueryLevels.mli
index bc1dc74149fa03284c1960b1485eba58511b964b..5b214b73364741d3dace7e1750cd612736d89e15 100644 (file)
--- a/helm/gTopLevel/mQueryLevels.mli
+++ b/helm/gTopLevel/mQueryLevels.mli
@@ -33,8 +33,4 @@
 (*                                                                            *)
 (******************************************************************************)
 
-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 out_restr: Cic.metasenv -> Cic.context -> Cic.term -> ( ((string * bool) list) list * (string * bool) list)