X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FmQueryLevels.mli;h=5b214b73364741d3dace7e1750cd612736d89e15;hb=7ff85e55518d06d96b9abbea4aa68d83e6be35b0;hp=82fb7c69998d4d56d67ca5f6b7accc19462b51fd;hpb=2208a75027ccad441dc0778101f57eff9555f8ea;p=helm.git

diff --git a/helm/gTopLevel/mQueryLevels.mli b/helm/gTopLevel/mQueryLevels.mli
index 82fb7c699..5b214b733 100644
--- 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