diff options
| author | Pierre Courtieu | 2015-10-19 18:12:27 +0200 |
|---|---|---|
| committer | Pierre Courtieu | 2015-10-19 18:14:26 +0200 |
| commit | 50a574f8b3e7f29550d7abf600d92eb43e7f8ef6 (patch) | |
| tree | fe31e7c529c914a1d7d42a77d9b60bdb390ff314 /tactics | |
| parent | b3b04d0a5c7c39140e2125321a17957ddcaf2b33 (diff) | |
Categorizing debug messages as such + NonLogical uses loggers.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacinterp.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 96d0b592b8..5a0d26a1cb 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -44,8 +44,8 @@ open Proofview.Notations let safe_msgnl s = Proofview.NonLogical.catch - (Proofview.NonLogical.print (s++fnl())) - (fun _ -> Proofview.NonLogical.print (str "bug in the debugger: an exception is raised while printing debug information"++fnl())) + (Proofview.NonLogical.print_debug (s++fnl())) + (fun _ -> Proofview.NonLogical.print_warning (str "bug in the debugger: an exception is raised while printing debug information"++fnl())) type value = tlevel generic_argument @@ -1136,7 +1136,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with interp_message ist s >>= fun msg -> return (hov 0 msg , hov 0 msg) in - let print (_,msgnl) = Proofview.(tclLIFT (NonLogical.print msgnl)) in + let print (_,msgnl) = Proofview.(tclLIFT (NonLogical.print_info msgnl)) in let log (msg,_) = Proofview.Trace.log (fun () -> msg) in let break = Proofview.tclLIFT (db_breakpoint (curr_debug ist) s) in Ftactic.run msgnl begin fun msgnl -> |