1 files changed, 13 insertions, 13 deletions

diff --git a/engine/namegen.ml b/engine/namegen.ml
index a75fe721f..489666852 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -239,7 +239,7 @@ let visible_ids sigma (nenv, c) =
 let next_name_away_in_cases_pattern sigma env_t na avoid =
   let id = match na with Name id -> id | Anonymous -> default_dependent_ident in
   let visible = visible_ids sigma env_t in
-  let bad id = Id.List.mem id avoid || is_constructor id
+  let bad id = Id.Set.mem id avoid || is_constructor id
                                     || Id.Set.mem id visible in
   next_ident_away_from id bad
 
@@ -253,8 +253,8 @@ let next_name_away_in_cases_pattern sigma 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 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
+  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 && not (is_section_variable id)) in
   next_ident_away_from id bad
 
 let next_name_away_in_goal na avoid =
@@ -271,16 +271,16 @@ let next_name_away_in_goal na avoid =
    beyond the current subscript *)
 
 let next_global_ident_away id avoid =
-  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
+  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
   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 Id.List.mem id avoid then
-    next_ident_away_from (restart_subscript id) (fun id -> Id.List.mem id avoid)
+  if Id.Set.mem id avoid then
+    next_ident_away_from (restart_subscript id) (fun id -> Id.Set.mem id avoid)
   else id
 
 let next_name_away_with_default default na avoid =
@@ -302,7 +302,7 @@ let next_name_away = next_name_away_with_default default_non_dependent_string
 
 let make_all_name_different env sigma =
   (** FIXME: this is inefficient, but only used in printing *)
-  let avoid = ref (Id.Set.elements (Context.Named.to_vars (named_context env))) in
+  let avoid = ref (Context.Named.to_vars (named_context env)) in
   let sign = named_context_val env in
   let rels = rel_context env in
   let env0 = reset_with_named_context sign env in
@@ -310,7 +310,7 @@ let make_all_name_different env sigma =
     (fun decl newenv ->
        let na = named_hd newenv sigma (RelDecl.get_type decl) (RelDecl.get_name decl) in
        let id = next_name_away na !avoid in
-       avoid := id::!avoid;
+       avoid := Id.Set.add id !avoid;
        push_rel (RelDecl.set_name (Name id) decl) newenv)
     rels ~init:env0
 
@@ -321,7 +321,7 @@ let make_all_name_different env sigma =
 
 let next_ident_away_for_default_printing sigma env_t id avoid =
   let visible = visible_ids sigma env_t in
-  let bad id = Id.List.mem id avoid || Id.Set.mem id visible in
+  let bad id = Id.Set.mem id avoid || Id.Set.mem id visible in
   next_ident_away_from id bad
 
 let next_name_away_for_default_printing sigma env_t na avoid =
@@ -371,7 +371,7 @@ let compute_displayed_name_in sigma flags avoid na c =
   | _ ->
     let fresh_id = next_name_for_display sigma flags na avoid in
     let idopt = if noccurn sigma 1 c then Anonymous else Name fresh_id in
-    (idopt, fresh_id::avoid)
+    (idopt, Id.Set.add fresh_id avoid)
 
 let compute_and_force_displayed_name_in sigma flags avoid na c =
   match na with
@@ -379,11 +379,11 @@ let compute_and_force_displayed_name_in sigma flags avoid na c =
     (Anonymous,avoid)
   | _ ->
     let fresh_id = next_name_for_display sigma flags na avoid in
-    (Name fresh_id, fresh_id::avoid)
+    (Name fresh_id, Id.Set.add fresh_id avoid)
 
 let compute_displayed_let_name_in sigma flags avoid na c =
   let fresh_id = next_name_for_display sigma flags na avoid in
-  (Name fresh_id, fresh_id::avoid)
+  (Name fresh_id, Id.Set.add fresh_id avoid)
 
 let rename_bound_vars_as_displayed sigma avoid env c =
   let rec rename avoid env c =