diff options
Diffstat (limited to 'printing/printer.ml')
| -rw-r--r-- | printing/printer.ml | 10 |
1 files changed, 1 insertions, 9 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index 1e4ef47095..d51174a42f 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -431,15 +431,7 @@ let pr_open_subgoals () = | [] -> let { Evd.it = bgoals ; sigma = bsigma } = Proof.V82.background_subgoals p in begin match bgoals with | [] -> pr_subgoals None sigma seeds goals - | _ -> pr_subgoals None bsigma seeds bgoals ++ fnl () ++ fnl () ++ - str"This subproof is complete, but there are still unfocused goals." - (* spiwack: to stay compatible with the proof general and coqide, - I use print the message after the goal. It would be better to have - something like: - str"This subproof is complete, but there are still unfocused goals:" - ++ fnl () ++ fnl () ++ pr_subgoals None bsigma bgoals - instead. But it doesn't quite work. - *) + | _ -> str"This subproof is complete, but there are still unfocused goals." ++ fnl () ++ fnl () ++ pr_subgoals None bsigma seeds bgoals end | _ -> pr_subgoals None sigma seeds goals end |