diff options
Diffstat (limited to 'printing/printer.ml')
| -rw-r--r-- | printing/printer.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index 5d9fa1313..7dfcde3ed 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -618,15 +618,15 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () = begin match bgoals,shelf,given_up with | [] , [] , [] -> pr_subgoals None sigma seeds shelf stack goals | [] , [] , _ -> - msg_warning (str "No more goals, however there are goals you gave up. You need to go back and solve them."); + msg_info (str "No more goals, however there are goals you gave up. You need to go back and solve them."); fnl () ++ fnl () ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] given_up | [] , _ , _ -> - msg_warning (str "All the remaining goals are on the shelf."); + msg_info (str "All the remaining goals are on the shelf."); fnl () ++ fnl () ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] shelf | _ , _, _ -> - msg_warning (str "This subproof is complete, but there are still unfocused goals."); + msg_info (str "This subproof is complete, but there are still unfocused goals."); fnl () ++ fnl () ++ pr_subgoals ~pr_first:false None bsigma seeds shelf [] bgoals end |