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/jall.ml | |
| 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/jall.ml')
| -rw-r--r-- | contrib/jprover/jall.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/contrib/jprover/jall.ml b/contrib/jprover/jall.ml index 77674c7b8..876dc6c06 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 |