X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FtopLevel%2FtopLevel.ml;h=745be0767a6b137a7937447e20b2757a5e929316;hb=4cbd4cadc2e71d4d25469dd7dddf05088baacb62;hp=cb7c7fca161eda84702293a64c61c0dc6144e761;hpb=2208a75027ccad441dc0778101f57eff9555f8ea;p=helm.git

diff --git a/helm/gTopLevel/topLevel/topLevel.ml b/helm/gTopLevel/topLevel/topLevel.ml
index cb7c7fca1..745be0767 100644
--- a/helm/gTopLevel/topLevel/topLevel.ml
+++ b/helm/gTopLevel/topLevel/topLevel.ml
@@ -73,18 +73,6 @@ let rec display = function
       print_string ("? " ^ CicPp.ppterm term ^ nl);
       flush stdout
 
-let levels l =
-   let module Lev = MQueryLevels in
-   let rec levels_aux = function
-      | []           -> ()
-      | term :: tail -> 
-         levels_aux tail;
-         print_string ("? " ^ CicPp.ppterm term ^ nl);
-         print_string (Lev.string_of_levels (Lev.levels_of_term [] [] term) nl);
-         flush stdout
-   in
-   levels_aux l
-
 let execute ich =
    let module Util = MQueryUtil in
    let module Gen = MQueryGenerator in
@@ -159,7 +147,6 @@ let prerr_help () =
    prerr_endline "-t  -typeof URI         outputs the CIC type of the given HELM object";
    prerr_endline "-x  -execute            issues a query given in the input file";
    prerr_endline "-d  -disply             outputs the CIC terms given in the input file";
-   prerr_endline "-l  -levels             outputs the cut levels of the CIC terms given in the input file";
    prerr_endline "-L  -locate ALIAS       issues the \"Locate\" query for the given alias";
    prerr_endline "-B  -backward LEVEL     issues the \"Backward\" query for the given level on all CIC terms";
    prerr_endline "                        in the input file";
@@ -175,7 +162,6 @@ let parse_args () =
       | ("-h"|"-help") :: rem -> prerr_help ()
       | ("-d"|"-display") :: rem -> display (get_terms ())
       | ("-t"|"-typeof") :: arg :: rem -> pp_type_of arg; parse rem
-      | ("-l"|"-levels") :: rem -> levels (get_terms ())
       | ("-x"|"-execute") :: rem -> execute stdin; parse rem
       | ("-q"|"-show-queries") :: rem -> show_queries := true; parse rem
       | ("-s"|"-stat") :: rem -> Mqint.set_stat true; parse rem