diff options
| author | Hugo Herbelin | 2020-12-18 18:57:25 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-12-18 18:57:25 +0100 |
| commit | 74ccd947d89e61ca1fc61575fe8012c2f8bd55fd (patch) | |
| tree | 86fcb2a3e4cf7823e094f734509401a46d0fc1ea /ide/coqide | |
| parent | 82d0a578b91f4de87deebc658b0e085646ca63d4 (diff) | |
Fixes #13657: vscoq needs goal uid.
Diffstat (limited to 'ide/coqide')
| -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 |