diff options
| author | Pierre Corbineau | 2014-12-16 15:59:52 +0100 |
|---|---|---|
| committer | Pierre Corbineau | 2014-12-16 16:01:25 +0100 |
| commit | 8029f7555f9c6f201cc70b5ecc538b11a861f0aa (patch) | |
| tree | c750b3ea7cafd5ec2176866bbd16208e5335978a /printing | |
| parent | d4f5bdd6f7304fac541bb5f4555ecdd6aa42699a (diff) | |
| parent | f88cce2698da000ab9054da31330db70997a41a4 (diff) | |
fix bug #2447 in congruence
Diffstat (limited to 'printing')
| -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 5d9fa13137..7dfcde3edb 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 |