diff options
| author | Vincent Laporte | 2019-02-14 11:17:35 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-02-18 08:19:23 +0000 |
| commit | 647c16764a497b922cc524ba4d956896caa5db5b (patch) | |
| tree | e0a97f1a3b86c21738e28bd88d4bc40016cb1e0f /engine | |
| parent | a49077ef67b8e70696ecacc311fc3070d1b7b461 (diff) | |
[Namegen] Use Global.exists_objlabel in `next_global_ident_away`
Fixes #9323.
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/namegen.ml | 2 |
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, |