From 456e2be8af1d4a0cf2461d62dc5e1b4b24b2a552 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Mon, 4 Jan 2016 18:04:18 +0100
Subject: Extraction: msg_notice instead of msg_info.

---
 plugins/extraction/extract_env.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 9964280336..657a91c0c1 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -542,7 +542,7 @@ let print_structure_to_file (fn,si,mo) dry struc =
     (if dry then None else si);
   (* Print the buffer content via Coq standard formatter (ok with coqide). *)
   if not (Int.equal (Buffer.length buf) 0) then begin
-    Pp.msg_info (str (Buffer.contents buf));
+    Pp.msg_notice (str (Buffer.contents buf));
     Buffer.reset buf
   end
 
@@ -636,7 +636,7 @@ let simple_extraction r =
       in
       let ans = flag ++ print_one_decl struc (modpath_of_r r) d in
       reset ();
-      Pp.msg_info ans
+      Pp.msg_notice ans
   | _ -> assert false
 
 
-- 
cgit v1.2.3