diff options
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." |