diff options
| author |  corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-30 16:23:38 +0000 |
|---|---|---|
| committer | corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-30 16:23:38 +0000 |
| commit | 0105110ddde98d5f49f5e7a5e52d5cce1f4bd8ca (patch) | |
| tree | 54a0655fa93061f24a56103de0d829400669db29 /contrib/jprover/jprover.ml4 | |
| parent | e52a9fa8835eddf70d0c8e454470fb12eebef7cd (diff) | |
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
Diffstat (limited to 'contrib/jprover/jprover.ml4')
| -rw-r--r-- | contrib/jprover/jprover.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/jprover/jprover.ml4 b/contrib/jprover/jprover.ml4 index 5fce08d38..dd76438f6 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." |