diff options
| author | Guillaume Melquiond | 2016-01-05 20:07:37 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2016-01-05 20:07:37 +0100 |
| commit | 7ca0319268c2c6912e08c53deb742d5f7631e210 (patch) | |
| tree | 5c9613224ca234af907374485b6f2241303e23ee /plugins/extraction | |
| parent | 5d26829704b2602ede45183cba54ab219e453c0e (diff) | |
| parent | e4a682e2f2c91fac47f55cd8619af2321b2e4c30 (diff) | |
Merge remote-tracking branch 'origin/v8.5' into trunk
Diffstat (limited to 'plugins/extraction')
| -rw-r--r-- | plugins/extraction/extract_env.ml | 4 |
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 |