diff options
Diffstat (limited to 'printing/printer.ml')
| -rw-r--r-- | printing/printer.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index 1425cebafc..ca9dee2df6 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -480,7 +480,7 @@ let pr_goal_name sigma g = let pr_goal_header nme sigma g = let (g,sigma) = Goal.V82.nf_evar sigma g in - str "subgoal " ++ nme ++ (if should_tag() then pr_goal_tag g else str"") + str "goal " ++ nme ++ (if should_tag() then pr_goal_tag g else str"") ++ (if should_gname() then str " " ++ Pp.surround (pr_existential_key sigma g) else mt ()) (* display the conclusion of a goal *) @@ -753,10 +753,10 @@ let pr_subgoals ?(pr_first=true) ?(diffs=false) ?os_map | [] -> let exl = Evd.undefined_map sigma in if Evar.Map.is_empty exl then - v 0 (str "No more subgoals." ++ pr_evar_info None sigma seeds) + v 0 (str "No more goals." ++ pr_evar_info None sigma seeds) else let pei = pr_evars_int sigma ~shelf ~given_up:[] 1 exl in - v 0 ((str "No more subgoals," + v 0 ((str "No more goals," ++ str " but there are non-instantiated existential variables:" ++ cut () ++ (hov 0 pei) ++ pr_evar_info None sigma seeds @@ -765,9 +765,9 @@ let pr_subgoals ?(pr_first=true) ?(diffs=false) ?os_map let goals = print_multiple_goals g1 rest in let ngoals = List.length rest+1 in v 0 ( - int ngoals ++ focused_if_needed ++ str(String.plural ngoals "subgoal") + int ngoals ++ focused_if_needed ++ str(String.plural ngoals "goal") ++ print_extra - ++ str (if pr_first && (should_gname()) && ngoals > 1 then ", subgoal 1" else "") + ++ str (if pr_first && (should_gname()) && ngoals > 1 then ", goal 1" else "") ++ (if pr_first && should_tag() then pr_goal_tag g1 else str"") ++ (if pr_first then pr_goal_name sigma g1 else mt()) ++ cut () ++ goals ++ (if unfocused=[] then str "" @@ -792,7 +792,7 @@ let pr_open_subgoals_diff ?(quiet=false) ?(diffs=false) ?oproof proof = begin match bgoals,shelf,given_up with | [] , [] , g when Evar.Set.is_empty g -> pr_subgoals None sigma ~seeds ~shelf ~stack ~unfocused:[] ~goals | [] , [] , _ -> - Feedback.msg_info (str "No more subgoals, but there are some goals you gave up:"); + Feedback.msg_info (str "No more goals, but there are some goals you gave up:"); fnl () ++ pr_subgoals ~pr_first:false None bsigma ~seeds ~shelf:[] ~stack:[] ~unfocused:[] ~goals:(Evar.Set.elements given_up) ++ fnl () ++ str "You need to go back and solve them." |