more fixes to the cleanu phase

[helm.git] / components / grafite_engine / grafiteEngine.ml

diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml
index dfe0c019f4833a06d2cf8fe309249455473b2ff5..409c0921aeb3f41b1876511fb95d2a2100921527 100644 (file)
--- a/components/grafite_engine/grafiteEngine.ml
+++ b/components/grafite_engine/grafiteEngine.ml
@@ -681,7 +681,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
      status,[]
   | GrafiteAst.Print (_,"proofterm") ->
       let _,_,_,p,_, _ = GrafiteTypes.get_current_proof status in
-      print_endline (Auto.pp_proofterm p);
+      prerr_endline (Auto.pp_proofterm p);
       status,[]
   | GrafiteAst.Print (_,_) -> status,[]
   | GrafiteAst.Qed loc ->