diff options
Diffstat (limited to 'dev/top_printers.ml')
| -rw-r--r-- | dev/top_printers.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml index f5599d793..4da901e53 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -29,7 +29,8 @@ let _ = set_bool_option_value ["Printing";"Matching"] false let _ = Detyping.set_detype_anonymous (fun _ _ -> raise Not_found) (* std_ppcmds *) -let pppp x = pp x +let pp x = Feedback.msg_notice x +let pppp x = Feedback.msg_notice x (** Future printer *) @@ -315,7 +316,7 @@ let constr_display csr = | Anonymous -> "Anonymous" in - Pp.pp (str (term_display csr) ++fnl ()); Pp.pp_flush () + Feedback.msg_notice (str (term_display csr) ++fnl ()) open Format;; @@ -515,7 +516,7 @@ let _ = (fun () -> in_current_context constr_display c) | _ -> failwith "Vernac extension: cannot occur") with - e -> Pp.pp (Errors.print e) + e -> Feedback.msg_notice (Errors.print e) let _ = extend_vernac_command_grammar ("PrintConstr", 0) None [GramTerminal "PrintConstr"; @@ -531,7 +532,7 @@ let _ = (fun () -> in_current_context print_pure_constr c) | _ -> failwith "Vernac extension: cannot occur") with - e -> Pp.pp (Errors.print e) + e -> Feedback.msg_notice (Errors.print e) let _ = extend_vernac_command_grammar ("PrintPureConstr", 0) None [GramTerminal "PrintPureConstr"; |