From 647c16764a497b922cc524ba4d956896caa5db5b Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Thu, 14 Feb 2019 11:17:35 +0000
Subject: [Namegen] Use Global.exists_objlabel in `next_global_ident_away`

Fixes #9323.
---
 engine/namegen.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'engine')

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