diff options
| -rw-r--r-- | ide/wg_ProofView.ml | 16 | ||||
| -rw-r--r-- | printing/printer.ml | 10 |
2 files changed, 12 insertions, 14 deletions
diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml index 1f3fa3ed3..69d460b01 100644 --- a/ide/wg_ProofView.ml +++ b/ide/wg_ProofView.ml @@ -140,20 +140,22 @@ let display mode (view : #GText.view_skel) goals hints evars = view#buffer#insert "No more subgoals." | [], [], [], _ :: _ -> (* A proof has been finished, but not concluded *) - view#buffer#insert "No more subgoals but non-instantiated existential variables:\n\n"; + view#buffer#insert "No more subgoals, but there are non-instantiated existential variables:\n\n"; let iter evar = let msg = Printf.sprintf "%s\n" evar.Interface.evar_info in view#buffer#insert msg in - List.iter iter evars + List.iter iter evars; + view#buffer#insert "\nYou can use Grab Existential Variables." | [], [], _, _ -> (* The proof is finished, with the exception of given up goals. *) - view#buffer#insert "No more, however there are goals you gave up. You need to go back and solve them:\n\n"; + view#buffer#insert "No more subgoals, but there are some goals you gave up:\n\n"; let iter goal = let msg = Printf.sprintf "%s\n" goal.Interface.goal_ccl in view#buffer#insert msg in - List.iter iter given_up_goals + List.iter iter given_up_goals; + view#buffer#insert "\nYou need to go back and solve them." | [], _, _, _ -> (* All the goals have been resolved but those on the shelf. *) view#buffer#insert "All the remaining goals are on the shelf:\n\n"; @@ -168,11 +170,7 @@ let display mode (view : #GText.view_skel) goals hints evars = let goal_str index = Printf.sprintf "______________________________________(%d/%d)\n" index total in - let vb, pl = if total = 1 then "is", "" else "are", "s" in - let msg = Printf.sprintf "This subproof is complete, but there %s still %d \ - unfocused goal%s:\n\n" vb total pl - in - let () = view#buffer#insert msg in + view#buffer#insert "This subproof is complete, but there are some unfocused goals:\n\n"; let iter i goal = let () = view#buffer#insert (goal_str (succ i)) in let msg = Printf.sprintf "%s\n" goal.Interface.goal_ccl in 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 () |