diff options
| author |  Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2015-10-02 14:41:57 +0200 |
|---|---|---|
| committer | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2015-10-02 14:41:57 +0200 |
| commit | 88abc50ece70405d71777d5350ca2fa70c1ff437 (patch) | |
| tree | a290d8f8cb67f0e337a23d71cbb308d444adaf10 | |
| parent | 832ef36c5b066f5cb50a85b9a1450eaf7dcb9e44 (diff) | |
Changed status of Info messages from notice to info.
This fixes a bug in proofgeneral. PG will now diplay this message
eagerly. Otherwise since they appear before the goal, they are
considered outdated and not displayed.
| -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 ceb4facc1..05a297545 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 |