CLEANUP: Namegen.to_avoid

This function does the same thing as "Names.Id.List.mem" so:
- I deleted the "Namegen.to_avoid" function and
- replaced all calls of "Namegen.to_avoid" to calls of "Names.Id.List.mem"

1 files changed, 9 insertions, 13 deletions

diff --git a/engine/namegen.ml b/engine/namegen.ml
index 8ab2fdd823..92a9151116 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -182,10 +182,6 @@ let restart_subscript id =
      *** make_ident id (Some 0) *** but compatibility would be lost... *)
     forget_subscript id
 
-let rec to_avoid id = function
-| [] -> false
-| id' :: avoid -> Id.equal id id' || to_avoid id avoid
-
 let visible_ids (nenv, c) =
   let accu = ref (Refset_env.empty, Int.Set.empty, Id.Set.empty) in
   let rec visible_ids n c = match kind_of_term c with
@@ -232,8 +228,8 @@ let visible_ids (nenv, c) =
 let next_name_away_in_cases_pattern env_t na avoid =
   let id = match na with Name id -> id | Anonymous -> default_dependent_ident in
   let visible = visible_ids env_t in
-  let bad id = to_avoid id avoid || is_constructor id
-                                 || Id.Set.mem id visible in
+  let bad id = Id.List.mem id avoid || is_constructor id
+                                    || Id.Set.mem id visible in
   next_ident_away_from id bad
 
 (* 2- Looks for a fresh name for introduction in goal *)
@@ -246,8 +242,8 @@ let next_name_away_in_cases_pattern env_t na avoid =
      name is taken by finding a free subscript starting from 0 *)
 
 let next_ident_away_in_goal id avoid =
-  let id = if to_avoid id avoid then restart_subscript id else id in
-  let bad id = to_avoid id avoid || (is_global id && not (is_section_variable id)) in
+  let id = if Id.List.mem id avoid then restart_subscript id else id in
+  let bad id = Id.List.mem id avoid || (is_global id && not (is_section_variable id)) in
   next_ident_away_from id bad
 
 let next_name_away_in_goal na avoid =
@@ -264,16 +260,16 @@ let next_name_away_in_goal na avoid =
    beyond the current subscript *)
 
 let next_global_ident_away id avoid =
-  let id = if to_avoid id avoid then restart_subscript id else id in
-  let bad id = to_avoid id avoid || is_global id in
+  let id = if Id.List.mem id avoid then restart_subscript id else id in
+  let bad id = Id.List.mem id avoid || is_global id in
   next_ident_away_from id bad
 
 (* 4- Looks for next fresh name outside a list; if name already used,
    looks for same name with lower available subscript *)
 
 let next_ident_away id avoid =
-  if to_avoid id avoid then
-    next_ident_away_from (restart_subscript id) (fun id -> to_avoid id avoid)
+  if Id.List.mem id avoid then
+    next_ident_away_from (restart_subscript id) (fun id -> Id.List.mem id avoid)
   else id
 
 let next_name_away_with_default default na avoid =
@@ -310,7 +306,7 @@ let make_all_name_different env =
 
 let next_ident_away_for_default_printing env_t id avoid =
   let visible = visible_ids env_t in
-  let bad id = to_avoid id avoid || Id.Set.mem id visible in
+  let bad id = Id.List.mem id avoid || Id.Set.mem id visible in
   next_ident_away_from id bad
 
 let next_name_away_for_default_printing env_t na avoid =