From 50a574f8b3e7f29550d7abf600d92eb43e7f8ef6 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Mon, 19 Oct 2015 18:12:27 +0200
Subject: Categorizing debug messages as such + NonLogical uses loggers.

---
 proofs/tactic_debug.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'proofs/tactic_debug.ml')

diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 667765dbf2..6d6215c521 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -33,7 +33,7 @@ let explain_logic_error = ref (fun e -> mt())
 let explain_logic_error_no_anomaly = ref (fun e -> mt())
 
 let msg_tac_debug s = Proofview.NonLogical.print_debug (s++fnl())
-let msg_tac_notice s = Proofview.NonLogical.print (s++fnl())
+let msg_tac_notice s = Proofview.NonLogical.print_notice (s++fnl())
 
 (* Prints the goal *)
 
@@ -122,7 +122,7 @@ let run ini =
   let open Proofview.NonLogical in
   if not ini then
     begin
-      Proofview.NonLogical.print (str"\b\r\b\r") >>
+      Proofview.NonLogical.print_notice (str"\b\r\b\r") >>
       !skipped >>= fun skipped ->
       msg_tac_debug (str "Executed expressions: " ++ int skipped ++ fnl())
     end >>
@@ -137,7 +137,7 @@ let rec prompt level =
   let runtrue = run true in
   begin
     let open Proofview.NonLogical in
-    Proofview.NonLogical.print (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ") >>
+    Proofview.NonLogical.print_notice (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ") >>
     let exit = (skip:=0) >> (skipped:=0) >> raise Sys.Break in
     Proofview.NonLogical.catch Proofview.NonLogical.read_line
       begin function (e, info) -> match e with
-- 
cgit v1.2.3