diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-06-19 13:49:26 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-06-19 13:49:26 +0200 |
| commit | 1e9ef2c64dcfa916ba3643b219040cd8dabfd48a (patch) | |
| tree | 4c42235cf5a29b4fa52609ba6411500751ff9564 /printing | |
| parent | 03d1fa42c17896cb9d767b509e05bd0db78cb7d2 (diff) | |
Make end-of-proof output consistent across toplevels.
Ideally, the code should be shared between the various toplevels, but this
is a lot more work than just fixing a few strings.
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/printer.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index 141ae145d..652542825 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -559,8 +559,8 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals ++ emacs_print_dependent_evars sigma seeds) else let pei = pr_evars_int sigma 1 exl in - (str "No more subgoals but non-instantiated existential " ++ - str "variables:" ++ fnl () ++ (hov 0 pei) + (str "No more subgoals, but there are non-instantiated existential variables:" + ++ fnl () ++ (hov 0 pei) ++ emacs_print_dependent_evars sigma seeds ++ fnl () ++ str "You can use Grab Existential Variables.") end @@ -625,17 +625,17 @@ 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_info (str "No more goals, however there are goals you gave up. You need to go back and solve them."); + msg_info (str "No more subgoals, but there are some goals you gave up:"); fnl () ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] given_up + ++ fnl () ++ str "You need to go back and solve them." | [] , _ , _ -> msg_info (str "All the remaining goals are on the shelf."); fnl () ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] shelf | _ , _, _ -> let end_cmd = - strbrk "This subproof is complete, but there are still \ - unfocused goals." ++ + 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) ++ fnl () |