From 74ccd947d89e61ca1fc61575fe8012c2f8bd55fd Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 18 Dec 2020 18:57:25 +0100
Subject: Fixes #13657: vscoq needs goal uid.

---
 ide/coqide/idetop.ml       | 2 +-
 ide/coqide/wg_ProofView.ml | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'ide')

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
-- 
cgit v1.2.3