diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coqide/idetop.ml | 2 | ||||
| -rw-r--r-- | ide/coqide/wg_ProofView.ml | 12 |
2 files changed, 7 insertions, 7 deletions
diff --git a/ide/coqide/idetop.ml b/ide/coqide/idetop.ml index 602acefa7c..528e2a756b 100644 --- a/ide/coqide/idetop.ml +++ b/ide/coqide/idetop.ml @@ -195,7 +195,7 @@ let concl_next_tac = let process_goal sigma g = let env = Goal.V82.env sigma g in let min_env = Environ.reset_context env in - let id = if Printer.print_goal_names () then Names.Id.to_string (Termops.evar_suggested_name g sigma) else "" in + let id = if Printer.print_goal_names () then Names.Id.to_string (Termops.evar_suggested_name g sigma) else Goal.uid g in let ccl = pr_letype_env ~goal_concl_style:true env sigma (Goal.V82.concl sigma g) in diff --git a/ide/coqide/wg_ProofView.ml b/ide/coqide/wg_ProofView.ml index 8e451c9917..fa37edd82b 100644 --- a/ide/coqide/wg_ProofView.ml +++ b/ide/coqide/wg_ProofView.ml @@ -66,11 +66,11 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals ~unfoc_goals hints = mat in let goals_cnt = List.length rem_goals + 1 in let head_str = Printf.sprintf - "%d subgoal%s\n" goals_cnt (if 1 < goals_cnt then "s" else "") + "%d goal%s\n" goals_cnt (if 1 < goals_cnt then "s" else "") in let goal_str ?(shownum=false) index total id = let annot = - if CString.is_empty id then if shownum then Printf.sprintf "(%d/%d)" index total else "" + if Option.has_some (int_of_string_opt id) (* some uid *) then if shownum then Printf.sprintf "(%d/%d)" index total else "" else Printf.sprintf "(?%s)" id in Printf.sprintf "______________________________________%s\n" annot in @@ -148,10 +148,10 @@ let display mode (view : #GText.view_skel) goals hints evars = let evars = match evars with None -> [] | Some evs -> evs in begin match (bg, shelved_goals,given_up_goals, evars) with | [], [], [], [] -> - view#buffer#insert "No more subgoals." + view#buffer#insert "No more goals." | [], [], [], _ :: _ -> (* A proof has been finished, but not concluded *) - view#buffer#insert "No more subgoals, but there are non-instantiated existential variables:\n\n"; + view#buffer#insert "No more goals, 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 @@ -160,7 +160,7 @@ let display mode (view : #GText.view_skel) goals hints 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 subgoals, but there are some goals you gave up:\n\n"; + view#buffer#insert "No more goals, but there are some goals you gave up:\n\n"; let iter goal = insert_xml view#buffer (Richpp.richpp_of_pp width goal.Interface.goal_ccl); view#buffer#insert "\n" @@ -180,7 +180,7 @@ let display mode (view : #GText.view_skel) goals hints evars = let total = List.length bg in let goal_str index id = let annot = - if CString.is_empty id then Printf.sprintf "(%d/%d)" index total + if Option.has_some (int_of_string_opt id) (* some uid *) then Printf.sprintf "(%d/%d)" index total else Printf.sprintf "(?%s)" id in Printf.sprintf "______________________________________%s\n" annot |