aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
authorPierre Courtieu2016-01-04 18:04:18 +0100
committerPierre Courtieu2016-01-04 18:06:49 +0100
commit456e2be8af1d4a0cf2461d62dc5e1b4b24b2a552 (patch)
treefad9c9b6dc28cf4d8d73dd1c28d2a81200ac750f /plugins
parentbb9acba7cfe83ba3a5116b0e7aa78ac7f1219f60 (diff)
Extraction: msg_notice instead of msg_info.
Diffstat (limited to 'plugins')
-rw-r--r--plugins/extraction/extract_env.ml4
1 files changed, 2 insertions, 2 deletions
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