New module for level management (was in MQueryGenerator)

[helm.git] / helm / gTopLevel / topLevel / topLevel.ml

diff --git a/helm/gTopLevel/topLevel/topLevel.ml b/helm/gTopLevel/topLevel/topLevel.ml
index d4af37c23e38cd3b16e9791329e5c665d359a558..4825c5b36c28a7f7ab47e2b679117797f674b560 100644 (file)
--- a/helm/gTopLevel/topLevel/topLevel.ml
+++ b/helm/gTopLevel/topLevel/topLevel.ml
@@ -74,13 +74,13 @@ let rec display = function
       flush stdout
 
 let levels l =
-   let module Gen = MQueryGenerator in
+   let module Lev = MQueryLevels in
    let rec levels_aux = function
       | []           -> ()
       | term :: tail -> 
          levels_aux tail;
          print_string ("? " ^ CicPp.ppterm term ^ nl);
-         print_string (Gen.string_of_levels (Gen.levels_of_term [] [] term) nl);
+         print_string (Lev.string_of_levels (Lev.levels_of_term [] [] term) nl);
          flush stdout
    in
    levels_aux l