From 6c0af6104d41762220a1d613d2331e7a0294df80 Mon Sep 17 00:00:00 2001
From: pboutill
Date: Mon, 14 Nov 2011 16:38:19 +0000
Subject: Bug 2636 - Move string_of_ppcmds to Pp

by Tom Prince

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14650 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/proof_global.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'proofs')

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 0f3fed7046..99552c5529 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -179,10 +179,9 @@ let check_no_pending_proof () =
   if not (there_are_pending_proofs ()) then
     ()
   else begin
-    pp_with Format.str_formatter
+    Util.error (Pp.string_of_ppcmds
       (str"Proof editing in progress" ++ (msg_proofs false) ++ fnl() ++
-       str"Use \"Abort All\" first or complete proof(s).")   ;
-    Util.error (Format.flush_str_formatter ())
+       str"Use \"Abort All\" first or complete proof(s)."))
   end
 
 
-- 
cgit v1.2.3