diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2015-06-23 15:28:36 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2015-06-23 15:29:29 +0200 |
| commit | b28bafb1d2003558c916c75d36784f94e9aa1684 (patch) | |
| tree | 73d616a542aa2d22c760cadb515fb43675115043 | |
| parent | 85fbcf9ed5c2f080e83f52fd2cd1791fb4172e74 (diff) | |
Fix `Pp` function used by the `Info` command.
I used a low-level function, now changed to `msg_notice`.
| -rw-r--r-- | proofs/pfedit.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index d1b6afe22..9c041d72c 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.ppnl (hov 0 (Proofview.Trace.pr_info ~lvl:i info)) + | Some i -> Pp.msg_notice (hov 0 (Proofview.Trace.pr_info ~lvl:i info)) in (p,status) with |