diff options
| author | corbinea | 2003-10-30 16:23:38 +0000 |
|---|---|---|
| committer | corbinea | 2003-10-30 16:23:38 +0000 |
| commit | 0105110ddde98d5f49f5e7a5e52d5cce1f4bd8ca (patch) | |
| tree | 54a0655fa93061f24a56103de0d829400669db29 /contrib | |
| 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')
| -rw-r--r-- | contrib/jprover/jall.ml | 5 | ||||
| -rw-r--r-- | contrib/jprover/jprover.ml4 | 4 |
2 files changed, 6 insertions, 3 deletions
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." |