aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/pfedit.ml
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/pfedit.ml')
-rw-r--r--proofs/pfedit.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 5367a907e..45af036fb 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -111,7 +111,7 @@ let solve ?with_end_tac gi info_lvl tac pr =
let () =
match info_lvl with
| None -> ()
- | Some i -> Pp.msg_info (hov 0 (Proofview.Trace.pr_info ~lvl:i info))
+ | Some i -> Feedback.msg_info (hov 0 (Proofview.Trace.pr_info ~lvl:i info))
in
(p,status)
with