- 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 82fb7c69998d4d56d67ca5f6b7accc19462b51fd..5b214b73364741d3dace7e1750cd612736d89e15 100644 (file)
--- a/helm/gTopLevel/mQueryLevels.mli
+++ b/helm/gTopLevel/mQueryLevels.mli
@@ -33,14 +33,4 @@
 (*                                                                            *)
 (******************************************************************************)
 
-(*type can_restrictions = (string * bool) list
-
-type must_restrictions = ((string * bool) list) list*)
-
-type levels_spec = (string * bool * int) list
-
-val levels_of_term: Cic.metasenv -> Cic.context -> Cic.term -> levels_spec
-
 val out_restr: Cic.metasenv -> Cic.context -> Cic.term -> ( ((string * bool) list) list * (string * bool) list)
-
-val string_of_levels  : levels_spec -> string -> string