Minor module re-organization:

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

diff --git a/helm/gTopLevel/sequentPp.ml b/helm/gTopLevel/sequentPp.ml
index ad8d5bd1d46ffdf0a089c16e6a80277f4e310a95..8cce6e1e39a116e8200bed2a35f2dc339e8841be 100644 (file)
--- a/helm/gTopLevel/sequentPp.ml
+++ b/helm/gTopLevel/sequentPp.ml
@@ -50,12 +50,11 @@ module TextualPp =
   exception NotImplemented;;
 
   let print_sequent (metano,context,goal) =
-   let module P = ProofEngine in
-    "\n" ^
-     let (output,pretty_printer_context_of_context) = print_context context in
-      output ^
-       "---------------------- ?" ^ string_of_int metano ^ "\n" ^
-        CicPp.pp goal pretty_printer_context_of_context
+   "\n" ^
+    let (output,pretty_printer_context_of_context) = print_context context in
+     output ^
+      "---------------------- ?" ^ string_of_int metano ^ "\n" ^
+       CicPp.pp goal pretty_printer_context_of_context
   ;;
  end
 ;;