From 0105110ddde98d5f49f5e7a5e52d5cce1f4bd8ca Mon Sep 17 00:00:00 2001
From: corbinea
Date: Thu, 30 Oct 2003 16:23:38 +0000
Subject: Redirected some of the verbose jprover output through the Pp module.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4746 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/jprover/jall.ml     | 5 ++++-
 contrib/jprover/jprover.ml4 | 4 ++--
 2 files changed, 6 insertions(+), 3 deletions(-)

(limited to 'contrib')

diff --git a/contrib/jprover/jall.ml b/contrib/jprover/jall.ml
index 77674c7b86..876dc6c060 100644
--- a/contrib/jprover/jall.ml
+++ b/contrib/jprover/jall.ml
@@ -4391,13 +4391,16 @@ let rec try_multiplicity mult_limit ftree ordering pos_n mult logic =
        | _ ->
             let new_mult = mult+1 in
             begin
+            Pp.msgnl (Pp.(++) (Pp.str "Multiplicity Fail: Trying new multiplicity ")
+            (Pp.int new_mult));
+(*
                Format.open_box 0;
                Format.force_newline ();
                Format.print_string "Multiplicity Fail: ";
                Format.print_string ("Try new multiplicity "^(string_of_int new_mult));
                Format.force_newline ();
                Format.print_flush ();
-
+*)
                let (new_ftree,new_ordering,new_pos_n) =
                   add_multiplicity ftree pos_n new_mult logic in
                if (new_ftree = ftree) then
diff --git a/contrib/jprover/jprover.ml4 b/contrib/jprover/jprover.ml4
index 5fce08d386..dd76438f68 100644
--- a/contrib/jprover/jprover.ml4
+++ b/contrib/jprover/jprover.ml4
@@ -497,11 +497,11 @@ let jp limits gls =
             let (il,tr) = build_jptree p in
                if (il = []) then
                begin
-                  print_string "Proof is built.\n";
+                  Pp.msgnl (Pp.str "Proof is built.");
                   do_coq_proof tr gls
                end
                else UT.error "Cannot reconstruct proof tree from JProver."
-        with e -> print_string "JProver fails to prove this:\n";
+        with e -> Pp.msgnl (Pp.str "JProver fails to prove this:");
                   JT.print_error_msg e;
                   UT.error "JProver terminated."
 
-- 
cgit v1.2.3