diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-01-02 17:57:06 +0100 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-01-02 17:57:06 +0100 |
| commit | 5d26829704b2602ede45183cba54ab219e453c0e (patch) | |
| tree | 25740e6ba9dde46217b6a8f18eb83292e6d450b5 /printing/printer.ml | |
| parent | 80bbdf335be5657f5ab33b4aa02e21420d341de2 (diff) | |
Use streams rather than strings to handle bullet suggestions.
Diffstat (limited to 'printing/printer.ml')
| -rw-r--r-- | printing/printer.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index 7c031ea53..b6dda93c2 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -639,8 +639,8 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () = | _ , _, _ -> let end_cmd = str "This subproof is complete, but there are some unfocused goals." ++ - (match Proof_global.Bullet.suggest p - with None -> str"" | Some s -> fnl () ++ str s) ++ + (let s = Proof_global.Bullet.suggest p in + if Pp.is_empty s then s else fnl () ++ s) ++ fnl () in pr_subgoals ~pr_first:false (Some end_cmd) bsigma seeds shelf [] bgoals |