-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
-