Merge PR #9577: [Namegen] Use Global.exists_objlabel in `next_global_ident_away`

Reviewed-by: maximedenes
Reviewed-by: ppedrot

1 files changed, 1 insertions, 1 deletions

diff --git a/engine/namegen.ml b/engine/namegen.ml
index 294b61fd3d..7ef4108c22 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -329,7 +329,7 @@ let next_name_away_in_goal na avoid =
 
 let next_global_ident_away id avoid =
   let id = if Id.Set.mem id avoid then restart_subscript id else id in
-  let bad id = Id.Set.mem id avoid || is_global id in
+  let bad id = Id.Set.mem id avoid || Global.exists_objlabel (Label.of_id id) in
   next_ident_away_from id bad
 
 (* 4- Looks for next fresh name outside a list; if name already used,