aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--proofs/pfedit.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index ceb4facc1e..05a2975458 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -108,7 +108,7 @@ let solve ?with_end_tac gi info_lvl tac pr =
let () =
match info_lvl with
| None -> ()
- | Some i -> Pp.msg_notice (hov 0 (Proofview.Trace.pr_info ~lvl:i info))
+ | Some i -> Pp.msg_info (hov 0 (Proofview.Trace.pr_info ~lvl:i info))
in
(p,status)
with