X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FsequentPp.ml;h=8cce6e1e39a116e8200bed2a35f2dc339e8841be;hb=60c66573ddcb1cea922095dfdc3a315d8d5012a1;hp=ad8d5bd1d46ffdf0a089c16e6a80277f4e310a95;hpb=95d791163d23738e82c4232598138f7cbab4207f;p=helm.git

diff --git a/helm/gTopLevel/sequentPp.ml b/helm/gTopLevel/sequentPp.ml
index ad8d5bd1d..8cce6e1e3 100644
--- 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
 ;;