diff options
Diffstat (limited to 'printing/printer.ml')
| -rw-r--r-- | printing/printer.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index 38b5e0bfdd..47cf2ac1f3 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -626,9 +626,10 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () = fnl () ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] shelf | _ , _, _ -> - msg_info (str "This subproof is complete, but there are still unfocused goals."); - fnl () - ++ pr_subgoals ~pr_first:false None bsigma seeds shelf [] bgoals + msg_info (str "This subproof is complete, but there are still unfocused goals." ++ + (match Proof_global.Bullet.suggest p + with None -> str"" | Some s -> fnl () ++ str s)); + fnl () ++ pr_subgoals ~pr_first:false None bsigma seeds shelf [] bgoals end | _ -> pr_subgoals None sigma seeds shelf stack goals end |