diff options
| -rw-r--r-- | ide/coqide/idetop.ml | 2 | ||||
| -rw-r--r-- | ide/coqide/wg_ProofView.ml | 4 |
2 files changed, 3 insertions, 3 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..01dfed0067 100644 --- a/ide/coqide/wg_ProofView.ml +++ b/ide/coqide/wg_ProofView.ml @@ -70,7 +70,7 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals ~unfoc_goals hints = mat 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 @@ -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 |