Efficient fresh name generation relying on sets.

The old algorithm was relying on list membership, which is O(n). This was
nefarious for terms with many binders. We use instead sets in O(log n).

60 files changed, 295 insertions, 284 deletions

diff --git a/API/API.mli b/API/API.mli
index 654d93485..536efea78 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -2751,15 +2751,15 @@ sig
       the whole identifier except for the {i subscript}.
 
       E.g. if we take [foo42], then [42] is the {i subscript}, and [foo] is the root. *)
-  val next_ident_away : Names.Id.t -> Names.Id.t list -> Names.Id.t
+  val next_ident_away : Names.Id.t -> Names.Id.Set.t -> Names.Id.t
 
   val hdchar : Environ.env -> Evd.evar_map -> EConstr.types -> string
   val id_of_name_using_hdchar : Environ.env -> Evd.evar_map -> EConstr.types -> Names.Name.t -> Names.Id.t
-  val next_ident_away_in_goal : Names.Id.t -> Names.Id.t list -> Names.Id.t
+  val next_ident_away_in_goal : Names.Id.t -> Names.Id.Set.t -> Names.Id.t
   val default_dependent_ident : Names.Id.t
-  val next_global_ident_away : Names.Id.t -> Names.Id.t list -> Names.Id.t
+  val next_global_ident_away : Names.Id.t -> Names.Id.Set.t -> Names.Id.t
   val rename_bound_vars_as_displayed :
-    Evd.evar_map -> Names.Id.t list -> Names.Name.t list -> EConstr.types -> EConstr.types
+    Evd.evar_map -> Names.Id.Set.t -> Names.Name.t list -> EConstr.types -> EConstr.types
 end
 
 module Termops :
@@ -4011,7 +4011,7 @@ sig
   | Later : [ `thunk ] delay
   val print_universes : bool ref
   val print_evar_arguments : bool ref
-  val detype : 'a delay -> ?lax:bool -> bool -> Names.Id.t list -> Environ.env -> Evd.evar_map -> EConstr.constr -> 'a Glob_term.glob_constr_g
+  val detype : 'a delay -> ?lax:bool -> bool -> Names.Id.Set.t -> Environ.env -> Evd.evar_map -> EConstr.constr -> 'a Glob_term.glob_constr_g
   val subst_glob_constr : Mod_subst.substitution -> Glob_term.glob_constr -> Glob_term.glob_constr
   val set_detype_anonymous : (?loc:Loc.t -> int -> Names.Id.t) -> unit
 end
@@ -4628,6 +4628,7 @@ sig
 
     val pf_env : 'a Proofview.Goal.t -> Environ.env
     val pf_ids_of_hyps : 'a Proofview.Goal.t -> Names.Id.t list
+    val pf_ids_set_of_hyps : 'a Proofview.Goal.t -> Names.Id.Set.t
     val pf_concl : 'a Proofview.Goal.t -> EConstr.types
     val pf_get_new_id  : Names.Id.t -> 'a Proofview.Goal.t -> Names.Id.t
     val pf_get_hyp_typ : Names.Id.t -> 'a Proofview.Goal.t -> EConstr.types
@@ -5140,7 +5141,7 @@ sig
   val convert_concl : ?check:bool -> EConstr.types -> Constr.cast_kind -> unit tactic
   val intro_using : Names.Id.t -> unit tactic
   val intro : unit tactic
-  val fresh_id_in_env : Names.Id.t list -> Names.Id.t -> Environ.env -> Names.Id.t
+  val fresh_id_in_env : Names.Id.Set.t -> Names.Id.t -> Environ.env -> Names.Id.t
   val is_quantified_hypothesis : Names.Id.t -> 'a Goal.t -> bool
   val tclABSTRACT : ?opaque:bool -> Names.Id.t option -> unit Proofview.tactic -> unit Proofview.tactic
   val intro_patterns : bool -> Tactypes.intro_patterns -> unit Proofview.tactic
@@ -5240,7 +5241,7 @@ sig
   val eapply_with_bindings  : EConstr.constr Misctypes.with_bindings -> unit Proofview.tactic
   val assert_by  : Names.Name.t -> EConstr.types -> unit Proofview.tactic ->
                    unit Proofview.tactic
-  val intro_avoiding : Names.Id.t list -> unit Proofview.tactic
+  val intro_avoiding : Names.Id.Set.t -> unit Proofview.tactic
   val pose_proof : Names.Name.t -> EConstr.constr -> unit Proofview.tactic
   val pattern_option :  (Locus.occurrences * EConstr.constr) list -> Locus.goal_location -> unit Proofview.tactic
   val compute_elim_sig : Evd.evar_map -> ?elimc:EConstr.constr Misctypes.with_bindings -> EConstr.types -> elim_scheme
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 =
diff --git a/engine/namegen.mli b/engine/namegen.mli
index 14846a918..6fde90a39 100644
--- a/engine/namegen.mli
+++ b/engine/namegen.mli
@@ -72,23 +72,22 @@ val next_ident_away_from : Id.t -> (Id.t -> bool) -> Id.t
     the whole identifier except for the {i subscript}.
 
     E.g. if we take [foo42], then [42] is the {i subscript}, and [foo] is the root. *)
-val next_ident_away : Id.t -> Id.t list -> Id.t
+val next_ident_away : Id.t -> Id.Set.t -> Id.t
 
 (** Avoid clashing with a name already used in current module *)
-val next_ident_away_in_goal : Id.t -> Id.t list -> Id.t
+val next_ident_away_in_goal : Id.t -> Id.Set.t -> Id.t
 
 (** Avoid clashing with a name already used in current module 
    but tolerate overwriting section variables, as in goals *)
-val next_global_ident_away : Id.t -> Id.t list -> Id.t
+val next_global_ident_away : Id.t -> Id.Set.t -> Id.t
 
 (** Default is [default_non_dependent_ident] *)
-val next_name_away  : Name.t -> Id.t list -> Id.t
+val next_name_away  : Name.t -> Id.Set.t -> Id.t
 
-val next_name_away_with_default : string -> Name.t -> Id.t list ->
-  Id.t
+val next_name_away_with_default : string -> Name.t -> Id.Set.t -> Id.t
 
 val next_name_away_with_default_using_types : string -> Name.t ->
-  Id.t list -> types -> Id.t
+  Id.Set.t -> types -> Id.t
 
 val set_reserved_typed_name : (types -> Name.t) -> unit
 
@@ -103,13 +102,13 @@ type renaming_flags =
 val make_all_name_different : env -> evar_map -> env
 
 val compute_displayed_name_in :
-  evar_map -> renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list
+  evar_map -> renaming_flags -> Id.Set.t -> Name.t -> constr -> Name.t * Id.Set.t
 val compute_and_force_displayed_name_in :
-  evar_map -> renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list
+  evar_map -> renaming_flags -> Id.Set.t -> Name.t -> constr -> Name.t * Id.Set.t
 val compute_displayed_let_name_in :
-  evar_map -> renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list
+  evar_map -> renaming_flags -> Id.Set.t -> Name.t -> constr -> Name.t * Id.Set.t
 val rename_bound_vars_as_displayed :
-  evar_map -> Id.t list -> Name.t list -> types -> types
+  evar_map -> Id.Set.t -> Name.t list -> types -> types
 
 (**********************************************************************)
 (* Naming strategy for arguments in Prop when eliminating inductive types *)
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index f5eff693f..f1bee65ef 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1087,7 +1087,7 @@ let extern_constr_gen lax goal_concl_style scopt env sigma t =
   (* Not "goal_concl_style" means do alpha-conversion avoiding only *)
   (* those goal/section/rel variables that occurs in the subterm under *)
   (* consideration; see namegen.ml for further details *)
-  let avoid = if goal_concl_style then ids_of_context env else [] in
+  let avoid = if goal_concl_style then vars_of_env env else Id.Set.empty in
   let r = Detyping.detype Detyping.Later ~lax:lax goal_concl_style avoid env sigma t in
   let vars = vars_of_env env in
   extern false (scopt,[]) vars r
@@ -1099,14 +1099,14 @@ let extern_constr ?(lax=false) goal_concl_style env sigma t =
   extern_constr_gen lax goal_concl_style None env sigma t
 
 let extern_type goal_concl_style env sigma t =
-  let avoid = if goal_concl_style then ids_of_context env else [] in
+  let avoid = if goal_concl_style then vars_of_env env else Id.Set.empty in
   let r = Detyping.detype Detyping.Later goal_concl_style avoid env sigma t in
   extern_glob_type (vars_of_env env) r
 
 let extern_sort sigma s = extern_glob_sort (detype_sort sigma s)
 
 let extern_closed_glob ?lax goal_concl_style env sigma t =
-  let avoid = if goal_concl_style then ids_of_context env else [] in
+  let avoid = if goal_concl_style then vars_of_env env else Id.Set.empty in
   let r =
     Detyping.detype_closed_glob ?lax goal_concl_style avoid env sigma t
   in
@@ -1177,15 +1177,15 @@ let rec glob_of_pat env sigma pat = DAst.make @@ match pat with
 	| _ -> anomaly (Pp.str "PCase with non-trivial predicate but unknown inductive.")
       in
       GCases (RegularStyle,rtn,[glob_of_pat env sigma tm,indnames],mat)
-  | PFix f -> DAst.get (Detyping.detype_names false [] env (Global.env()) sigma (EConstr.of_constr (mkFix f))) (** FIXME bad env *)
-  | PCoFix c -> DAst.get (Detyping.detype_names false [] env (Global.env()) sigma (EConstr.of_constr (mkCoFix c)))
+  | PFix f -> DAst.get (Detyping.detype_names false Id.Set.empty env (Global.env()) sigma (EConstr.of_constr (mkFix f))) (** FIXME bad env *)
+  | PCoFix c -> DAst.get (Detyping.detype_names false Id.Set.empty env (Global.env()) sigma (EConstr.of_constr (mkCoFix c)))
   | PSort s -> GSort s
 
 let extern_constr_pattern env sigma pat =
   extern true (None,[]) Id.Set.empty (glob_of_pat env sigma pat)
 
 let extern_rel_context where env sigma sign =
-  let a = detype_rel_context Detyping.Later where [] (names_of_rel_context env,env) sigma sign in
+  let a = detype_rel_context Detyping.Later where Id.Set.empty (names_of_rel_context env,env) sigma sign in
   let vars = vars_of_env env in
   let a = List.map (extended_glob_local_binder_of_decl) a in
   pi3 (extern_local_binder (None,[]) vars a)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 6f7c6c827..1cea307d7 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -469,8 +469,7 @@ let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = functio
         | _ -> assert false
       in
       let env = {env with ids = List.fold_right Id.Set.add il env.ids} in
-      let ienv = Id.Set.elements env.ids in
-      let id = Namegen.next_ident_away (Id.of_string "pat") ienv in
+      let id = Namegen.next_ident_away (Id.of_string "pat") env.ids in
       let na = (loc, Name id) in
       let bk = Default Explicit in
       let _, bl' = intern_assumption intern lvar env [na] bk tyc in
@@ -1939,13 +1938,13 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
                 | _ ->
                   let fresh =
                     Namegen.next_name_away_with_default_using_types "iV" cano_name forbidden_names (EConstr.of_constr ty) in
-                  canonize_args t tt (fresh::forbidden_names)
+                  canonize_args t tt (Id.Set.add fresh forbidden_names)
                     ((fresh,c)::match_acc) ((cases_pattern_loc c,Name fresh)::var_acc)
                 end
 	      | _ -> assert false in
 	  let _,args_rel =
 	    List.chop nparams (List.rev mip.Declarations.mind_arity_ctxt) in
-	  canonize_args args_rel l (Id.Set.elements forbidden_names_for_gen) [] [] in
+	  canonize_args args_rel l forbidden_names_for_gen [] [] in
 	match_to_do, Some (cases_pattern_expr_loc t,(ind,List.rev_map snd nal))
     | None ->
       [], None in
diff --git a/interp/impargs.ml b/interp/impargs.ml
index d8241c044..09a0ba83c 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -255,7 +255,7 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t =
   in
   match kind_of_term (whd_all env t) with
     | Prod (na,a,b) ->
-	let na',avoid = find_displayed_name_in all [] na ([],b) in
+	let na',avoid = find_displayed_name_in all Id.Set.empty na ([],b) in
 	let v = aux (push_rel (LocalAssum (na',a)) env) avoid 1 [na'] b in
 	!rigid, Array.to_list v
     | _ -> true, []
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 3d48114ec..0967d21f0 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -577,7 +577,7 @@ let rec subst_notation_constr subst bound raw =
       if r1' == r1 && k' == k then raw else NCast(r1',k')
 
 let subst_interpretation subst (metas,pat) =
-  let bound = List.map fst metas in
+  let bound = List.fold_left (fun accu (id, _) -> Id.Set.add id accu) Id.Set.empty metas in
   (metas,subst_notation_constr subst bound pat)
 
 (**********************************************************************)
@@ -1143,7 +1143,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
      to print "{x:_ & P x}" knowing that notation "{x & P x}" is not defined. *)
   | _b1, NLambda (Name id as na,(NHole _ | NVar _ as t2),b2) when inner ->
       let avoid =
-        free_glob_vars a1 @ (* as in Namegen: *) glob_visible_short_qualid a1 in
+        Id.Set.union (free_glob_vars a1) (* as in Namegen: *) (glob_visible_short_qualid a1) in
       let id' = Namegen.next_ident_away id avoid in
       let t1 = DAst.make @@ GHole(Evar_kinds.BinderType (Name id'),Misctypes.IntroAnonymous,None) in
       let sigma = match t2 with
diff --git a/interp/reserve.ml b/interp/reserve.ml
index a1e5bd0ea..dc0f60dcf 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -110,7 +110,7 @@ let revert_reserved_type t =
     let t = EConstr.Unsafe.to_constr t in
     let reserved = KeyMap.find (constr_key t) !reserve_revtable in
     let t = EConstr.of_constr t in
-    let t = Detyping.detype Detyping.Now false [] (Global.env()) Evd.empty t in
+    let t = Detyping.detype Detyping.Now false Id.Set.empty (Global.env()) Evd.empty t in
     (* pedrot: if [Notation_ops.match_notation_constr] may raise [Failure _]
         then I've introduced a bug... *)
     let filter _ pat =
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 4a59b8597..819d236cd 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -131,7 +131,7 @@ let test_plural_form_types loc kwd = function
 
 let fresh_var env c =
   Namegen.next_ident_away (Id.of_string "pat")
-    (env @ Id.Set.elements (Topconstr.free_vars_of_constr_expr c))
+    (List.fold_left (fun accu id -> Id.Set.add id accu) (Topconstr.free_vars_of_constr_expr c) env)
 
 let _ = Hook.set Constrexpr_ops.fresh_var_hook fresh_var
 
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index fca7d9851..150319f6b 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -444,7 +444,7 @@ let cc_tactic depth additionnal_terms =
             let terms_to_complete = List.map (build_term_to_complete uf) (epsilons uf) in
             let hole = DAst.make @@ GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None) in
             let pr_missing (c, missing) =
-              let c = Detyping.detype Detyping.Now ~lax:true false [] env sigma c in
+              let c = Detyping.detype Detyping.Now ~lax:true false Id.Set.empty env sigma c in
               let holes = List.init missing (fun _ -> hole) in
               Printer.pr_glob_constr_env env (DAst.make @@ GApp (c, holes))
             in
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 9772ebd64..9aec190d0 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -405,7 +405,7 @@ let ref_renaming_fun (k,r) =
     let idg = safe_basename_of_global r in
     match l with
     | [""] -> (* this happens only at toplevel of the monolithic case *)
-      let globs = Id.Set.elements (get_global_ids ()) in
+      let globs = get_global_ids () in
       let id = next_ident_away (kindcase_id k idg) globs in
       Id.to_string id
     | _ -> modular_rename k idg
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 7644b49ce..a227478d0 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -141,6 +141,7 @@ let make_typvar n vl =
     if not (String.contains s '\'') && Unicode.is_basic_ascii s then id
     else id_of_name Anonymous
   in
+  let vl = Id.Set.of_list vl in
   next_ident_away id' vl
 
 let rec type_sign_vl env c =
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index ca98f07e8..30e3b520f 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -750,11 +750,11 @@ let extraction_implicit r l =
 
 let blacklist_table = Summary.ref Id.Set.empty ~name:"ExtrBlacklist"
 
-let modfile_ids = ref []
+let modfile_ids = ref Id.Set.empty
 let modfile_mps = ref MPmap.empty
 
 let reset_modfile () =
-  modfile_ids := Id.Set.elements !blacklist_table;
+  modfile_ids := !blacklist_table;
   modfile_mps := MPmap.empty
 
 let string_of_modfile mp =
@@ -763,7 +763,7 @@ let string_of_modfile mp =
     let id = Id.of_string (raw_string_of_modfile mp) in
     let id' = next_ident_away id !modfile_ids in
     let s' = Id.to_string id' in
-    modfile_ids := id' :: !modfile_ids;
+    modfile_ids := Id.Set.add id' !modfile_ids;
     modfile_mps := MPmap.add mp s' !modfile_mps;
     s'
 
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 169073630..c2606dbe8 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -115,8 +115,8 @@ let mk_open_instance env evmap id idc m t =
       let nid=(fresh_id_in_env avoid var_id env) in
       let (evmap, (c, _)) = Evarutil.new_type_evar env evmap Evd.univ_flexible in
       let decl = LocalAssum (Name nid, c) in
-	aux (n-1) (nid::avoid) (EConstr.push_rel decl env) evmap (decl::decls) in
-  let evmap, decls = aux m [] env evmap [] in
+	aux (n-1) (Id.Set.add nid avoid) (EConstr.push_rel decl env) evmap (decl::decls) in
+  let evmap, decls = aux m Id.Set.empty env evmap [] in
   (evmap, decls, revt)
 
 (* tactics   *)
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 5f6d78359..bd5fb1d92 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -587,7 +587,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
     tclTHENLIST
       [
 	(* We first introduce the variables *)
-	tclDO nb_first_intro (Proofview.V82.of_tactic (intro_avoiding dyn_infos.rec_hyps));
+	tclDO nb_first_intro (Proofview.V82.of_tactic (intro_avoiding (Id.Set.of_list dyn_infos.rec_hyps)));
 	(* Then the equation itself *)
 	Proofview.V82.of_tactic (intro_using heq_id);
 	onLastHypId (fun heq_id -> tclTHENLIST [
@@ -1614,7 +1614,7 @@ let prove_principle_for_gen
       let hid =
 	next_ident_away_in_goal
 	  (Id.of_string "prov")
-	  hyps
+	  (Id.Set.of_list hyps)
       in
       tclTHENLIST
 	[
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 409bb89ee..018b51517 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -39,7 +39,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
     | decl :: predicates ->
        (match Context.Rel.Declaration.get_name decl with
 	| Name x ->
-	   let id = Namegen.next_ident_away x avoid in
+	   let id = Namegen.next_ident_away x (Id.Set.of_list avoid) in
 	   Hashtbl.add tbl id x;
 	   RelDecl.set_name (Name id) decl :: change_predicates_names (id::avoid) predicates
 	| Anonymous -> anomaly (Pp.str "Anonymous property binder."))
@@ -285,7 +285,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
   (*    let time2 = System.get_time ()  in *)
   (*    Pp.msgnl (str "computing principle type := " ++ System.fmt_time_difference time1 time2); *)
   let new_princ_name =
-    next_ident_away_in_goal (Id.of_string "___________princ_________") []
+    next_ident_away_in_goal (Id.of_string "___________princ_________") Id.Set.empty
   in
   let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd (EConstr.of_constr new_principle_type) in
   let hook = Lemmas.mk_hook (hook new_principle_type) in
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 7087a195e..e8e5bfccc 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -120,13 +120,13 @@ let combine_args arg args =
 
 
 let ids_of_binder =  function
-  | LetIn Anonymous | Prod Anonymous | Lambda Anonymous -> []
-  | LetIn (Name id)  | Prod (Name id) | Lambda (Name id) -> [id]
+  | LetIn Anonymous | Prod Anonymous | Lambda Anonymous -> Id.Set.empty
+  | LetIn (Name id)  | Prod (Name id) | Lambda (Name id) -> Id.Set.singleton id
 
 let rec change_vars_in_binder mapping = function
     [] -> []
   | (bt,t)::l ->
-      let new_mapping = List.fold_right Id.Map.remove (ids_of_binder bt) mapping in
+      let new_mapping = Id.Set.fold Id.Map.remove (ids_of_binder bt) mapping in
       (bt,change_vars mapping t)::
 	(if Id.Map.is_empty new_mapping
 	 then l
@@ -137,27 +137,27 @@ let rec replace_var_by_term_in_binder x_id term = function
   | [] -> []
   | (bt,t)::l ->
       (bt,replace_var_by_term x_id term t)::
-	if Id.List.mem x_id (ids_of_binder bt)
+	if Id.Set.mem x_id (ids_of_binder bt)
 	then l
 	else replace_var_by_term_in_binder x_id term l
 
-let add_bt_names bt = List.append (ids_of_binder bt)
+let add_bt_names bt = Id.Set.union (ids_of_binder bt)
 
 let apply_args ctxt body args =
   let need_convert_id avoid id =
-    List.exists (is_free_in id) args || Id.List.mem id avoid
+    List.exists (is_free_in id) args || Id.Set.mem id avoid
   in
   let need_convert avoid  bt =
-    List.exists (need_convert_id avoid) (ids_of_binder bt)
+    Id.Set.exists (need_convert_id avoid) (ids_of_binder bt)
   in
-  let next_name_away (na:Name.t) (mapping: Id.t Id.Map.t) (avoid: Id.t list) =
+  let next_name_away (na:Name.t) (mapping: Id.t Id.Map.t) (avoid: Id.Set.t) =
     match na with
-       | Name id when Id.List.mem id avoid ->
+       | Name id when Id.Set.mem id avoid ->
 	   let new_id = Namegen.next_ident_away id avoid in
-	   Name new_id,Id.Map.add id new_id mapping,new_id::avoid
+	   Name new_id,Id.Map.add id new_id mapping,Id.Set.add new_id avoid
        | _ -> na,mapping,avoid
   in
-  let next_bt_away bt (avoid:Id.t list) =
+  let next_bt_away bt (avoid:Id.Set.t) =
     match bt with
       | LetIn na ->
 	  let new_na,mapping,new_avoid = next_name_away na Id.Map.empty avoid  in
@@ -182,15 +182,15 @@ let apply_args ctxt body args =
 	  let new_avoid,new_ctxt',new_body,new_id =
 	    if need_convert_id avoid id
 	    then
-	      let new_avoid =  id::avoid in
+	      let new_avoid =  Id.Set.add id avoid in
 	      let new_id = Namegen.next_ident_away id new_avoid in
-	      let new_avoid' = new_id :: new_avoid in
+	      let new_avoid' = Id.Set.add new_id new_avoid in
 	      let mapping = Id.Map.add id new_id Id.Map.empty in
 	      let new_ctxt' = change_vars_in_binder mapping ctxt' in
 	      let new_body = change_vars mapping body in
 	      new_avoid',new_ctxt',new_body,new_id
 	    else
-	      id::avoid,ctxt',body,id
+	      Id.Set.add id avoid,ctxt',body,id
 	  in
 	  let new_body = replace_var_by_term new_id arg new_body in
 	  let new_ctxt' = replace_var_by_term_in_binder new_id arg new_ctxt' in
@@ -214,7 +214,7 @@ let apply_args ctxt body args =
 	  in
 	  (new_bt,t)::new_ctxt',new_body
   in
-  do_apply []  ctxt body args
+  do_apply Id.Set.empty ctxt body args
 
 
 let combine_app f args =
@@ -434,7 +434,7 @@ let rec pattern_to_term_and_type env typ  = DAst.with_val (function
 	Array.to_list
 	  (Array.init
 	     (cst_narg - List.length patternl)
-	     (fun i -> Detyping.detype Detyping.Now false [] env (Evd.from_env env) (EConstr.of_constr csta.(i)))
+	     (fun i -> Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_env env) (EConstr.of_constr csta.(i)))
 	  )
       in
       let patl_as_term =
@@ -519,7 +519,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
 		*)
 		let rt_as_constr,ctx = Pretyping.understand env (Evd.from_env env) rt in
 		let rt_typ = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr rt_as_constr) in
-		let res_raw_type = Detyping.detype Detyping.Now false [] env (Evd.from_env env) rt_typ in
+		let res_raw_type = Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_env env) rt_typ in
 		let res = fresh_id args_res.to_avoid "_res" in
 		let new_avoid = res::args_res.to_avoid in
 		let res_rt = mkGVar res in
@@ -559,7 +559,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
 		  match n with
 		    | Name id when List.exists (is_free_in id) args ->
 			(* need to alpha-convert the name *)
-			let new_id = Namegen.next_ident_away id avoid in
+			let new_id = Namegen.next_ident_away id (Id.Set.of_list avoid) in
 			let new_avoid = id:: avoid in
 			let new_b =
 			  replace_var_by_term
@@ -773,7 +773,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 			  Typing.unsafe_type_of env_with_pat_ids (Evd.from_env env) (EConstr.mkVar id)
 			in
 			let raw_typ_of_id =
-			  Detyping.detype Detyping.Now false []
+			  Detyping.detype Detyping.Now false Id.Set.empty
 			    env_with_pat_ids (Evd.from_env env) typ_of_id
 			in
 			mkGProd (Name id,raw_typ_of_id,acc))
@@ -819,7 +819,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 	      (fun pat e typ_as_constr ->
 		 let this_pat_ids = ids_of_pat pat in
 		 let typ_as_constr = EConstr.of_constr typ_as_constr in
-		 let typ = Detyping.detype Detyping.Now false [] new_env (Evd.from_env env) typ_as_constr in
+		 let typ = Detyping.detype Detyping.Now false Id.Set.empty new_env (Evd.from_env env) typ_as_constr in
 		 let pat_as_term = pattern_to_term pat in
                  (* removing trivial holes *) 
                  let pat_as_term = solve_trivial_holes pat_as_term e in 
@@ -833,7 +833,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 		      then (Prod (Name id),
 		      let typ_of_id = Typing.unsafe_type_of new_env (Evd.from_env env) (EConstr.mkVar id) in
 		      let raw_typ_of_id =
-			Detyping.detype Detyping.Now false [] new_env (Evd.from_env env) typ_of_id
+			Detyping.detype Detyping.Now false Id.Set.empty new_env (Evd.from_env env) typ_of_id
 		      in
 		      raw_typ_of_id
 			   )::acc
@@ -1001,7 +1001,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		    let rt_typ = DAst.make @@
 		       GApp(DAst.make @@ GRef (Globnames.IndRef (fst ind),None),
 			    (List.map
-			      (fun p -> Detyping.detype Detyping.Now false []
+			      (fun p -> Detyping.detype Detyping.Now false Id.Set.empty
 				 env (Evd.from_env env)
 				 (EConstr.of_constr p)) params)@(Array.to_list
 				      (Array.make
@@ -1028,12 +1028,12 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 				   match na with
 				     | Anonymous -> acc
 				     | Name id' ->
-					 (id',Detyping.detype Detyping.Now false []
+					 (id',Detyping.detype Detyping.Now false Id.Set.empty
 					    env
                                             (Evd.from_env env)
 					    arg)::acc
 				 else if isVar var_as_constr
-				 then (destVar var_as_constr,Detyping.detype Detyping.Now false []
+				 then (destVar var_as_constr,Detyping.detype Detyping.Now false Id.Set.empty
 					 env
                                          (Evd.from_env env)
 					 arg)::acc
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 02ee56ac5..0666ab4f1 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -198,7 +198,7 @@ let rec alpha_pat excluded pat =
     | PatVar(Name id) ->
 	if Id.List.mem id excluded
 	then
-	  let new_id = Namegen.next_ident_away id excluded in
+	  let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in
 	  (DAst.make ?loc @@ PatVar(Name new_id)),(new_id::excluded),
 	(Id.Map.add id new_id Id.Map.empty)
 	else pat, excluded,Id.Map.empty
@@ -206,7 +206,7 @@ let rec alpha_pat excluded pat =
 	let new_na,new_excluded,map =
 	  match na with
 	    | Name id when Id.List.mem id excluded ->
-		let new_id = Namegen.next_ident_away id excluded in
+		let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in
 		Name new_id,new_id::excluded, Id.Map.add id new_id Id.Map.empty
 	    | _ -> na,excluded,Id.Map.empty
 	in
@@ -261,7 +261,7 @@ let rec alpha_rt excluded rt =
     match DAst.get rt with
       | GRef _ | GVar _ | GEvar _ | GPatVar _ as rt -> rt
       | GLambda(Anonymous,k,t,b) ->
-	  let new_id = Namegen.next_ident_away (Id.of_string "_x") excluded in
+	  let new_id = Namegen.next_ident_away (Id.of_string "_x") (Id.Set.of_list excluded) in
 	  let new_excluded = new_id :: excluded in
 	  let new_t = alpha_rt new_excluded t in
 	  let new_b = alpha_rt new_excluded b in
@@ -276,7 +276,7 @@ let rec alpha_rt excluded rt =
 	let new_c = alpha_rt excluded c in
 	GLetIn(Anonymous,new_b,new_t,new_c)
     | GLambda(Name id,k,t,b) ->
-	let new_id = Namegen.next_ident_away id excluded in
+	let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in
 	let t,b =
 	  if Id.equal new_id id
 	  then t, b
@@ -289,7 +289,7 @@ let rec alpha_rt excluded rt =
 	let new_b = alpha_rt new_excluded b in
 	GLambda(Name new_id,k,new_t,new_b)
     | GProd(Name id,k,t,b) ->
-	let new_id = Namegen.next_ident_away id excluded in
+	let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in
 	let new_excluded = new_id::excluded in
 	let t,b =
 	  if Id.equal new_id id
@@ -302,7 +302,7 @@ let rec alpha_rt excluded rt =
 	let new_b = alpha_rt new_excluded b in
 	GProd(Name new_id,k,new_t,new_b)
     | GLetIn(Name id,b,t,c) ->
-	let new_id = Namegen.next_ident_away id excluded in
+	let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in
 	let c =
 	  if Id.equal new_id id then c
 	  else change_vars (Id.Map.add id new_id Id.Map.empty) c
@@ -320,7 +320,7 @@ let rec alpha_rt excluded rt =
 	       match na with
 		 | Anonymous -> (na::nal,excluded,mapping)
 		 | Name id ->
-		     let new_id = Namegen.next_ident_away id excluded in
+		     let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in
 		     if Id.equal new_id id
 		     then
 		       na::nal,id::excluded,mapping
@@ -741,7 +741,7 @@ If someone knows how to prevent solved existantial removal in  understand, pleas
            match evi.evar_body with
            | Evar_defined c ->
            (* we just have to lift the solution in glob_term *)
-              Detyping.detype Detyping.Now false [] env ctx (EConstr.of_constr (f c))
+              Detyping.detype Detyping.Now false Id.Set.empty env ctx (EConstr.of_constr (f c))
            | Evar_empty -> rt (* the hole was not solved : we do nothing *)
        )
     | (GHole(BinderType na,_,_)) -> (* we only want to deal with implicit arguments *)
@@ -763,7 +763,7 @@ If someone knows how to prevent solved existantial removal in  understand, pleas
                 match evi.evar_body with
                 | Evar_defined c ->
                    (* we just have to lift the solution in glob_term *)
-                   Detyping.detype Detyping.Now false [] env ctx (EConstr.of_constr (f c))
+                   Detyping.detype Detyping.Now false Id.Set.empty env ctx (EConstr.of_constr (f c))
                 | Evar_empty -> rt (* the hole was not solved : we d when falseo nothing *)
          in 
          res
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 5f4d514f3..1e8854249 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -12,7 +12,7 @@ let mk_equation_id id = Nameops.add_suffix id "_equation"
 let msgnl m =
   ()
 
-let fresh_id avoid s = Namegen.next_ident_away_in_goal (Id.of_string s) avoid
+let fresh_id avoid s = Namegen.next_ident_away_in_goal (Id.of_string s) (Id.Set.of_list avoid)
 
 let fresh_name avoid s = Name (fresh_id avoid s)
 
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 5f8d50da1..299753766 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -131,9 +131,9 @@ let generate_type evd g_to_f f graph i =
 			   | Name id -> Some id
 			   | Anonymous -> None
   in
-  let named_ctxt = List.map_filter filter fun_ctxt in
+  let named_ctxt = Id.Set.of_list (List.map_filter filter fun_ctxt) in
   let res_id = Namegen.next_ident_away_in_goal (Id.of_string "_res") named_ctxt in
-  let fv_id = Namegen.next_ident_away_in_goal (Id.of_string "fv") (res_id :: named_ctxt) in
+  let fv_id = Namegen.next_ident_away_in_goal (Id.of_string "fv") (Id.Set.add res_id named_ctxt) in
   (*i we can then type the argument to be applied to the function [f] i*)
   let args_as_rels = Array.of_list (args_from_decl 1 [] fun_ctxt) in
   (*i
@@ -189,7 +189,7 @@ let rec generate_fresh_id x avoid i =
   if i == 0
   then []
   else
-    let id = Namegen.next_ident_away_in_goal x avoid in
+    let id = Namegen.next_ident_away_in_goal x (Id.Set.of_list avoid) in
     id::(generate_fresh_id x (id::avoid) (pred i))
 
 
@@ -239,7 +239,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
        environment and due to the bug #1174, we will need to pose the principle
        using a name
     *)
-    let principle_id = Namegen.next_ident_away_in_goal (Id.of_string "princ") ids in
+    let principle_id = Namegen.next_ident_away_in_goal (Id.of_string "princ") (Id.Set.of_list ids) in
     let ids = principle_id :: ids in
     (* We get the branches of the principle *)
     let branches = List.rev princ_infos.branches in
@@ -396,7 +396,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
       let params_bindings,avoid =
 	List.fold_left2
 	  (fun (bindings,avoid) decl p ->
-	     let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) avoid in
+	     let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) (Id.Set.of_list avoid) in
 	     p::bindings,id::avoid
 	  )
 	  ([],pf_ids_of_hyps g)
@@ -406,7 +406,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
       let lemmas_bindings =
 	List.rev (fst  (List.fold_left2
 	  (fun (bindings,avoid) decl p ->
-	     let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) avoid in
+	     let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) (Id.Set.of_list avoid) in
 	     (nf_zeta p)::bindings,id::avoid)
 	  ([],avoid)
 	  princ_infos.predicates
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 96200a98a..77c26f8ce 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -767,7 +767,7 @@ let merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body)
     (* first replace rel 1 by a varname *)
     let substindtyp = substitterm 0 (mkRel 1) (mkVar nme) typ in
     let substindtyp = EConstr.of_constr substindtyp in
-    Detyping.detype Detyping.Now false (Id.Set.elements avoid) (Global.env()) Evd.empty substindtyp in
+    Detyping.detype Detyping.Now false avoid (Global.env()) Evd.empty substindtyp in
   let lcstr1: glob_constr list =
     Array.to_list (Array.map (mkrawcor ind1name avoid) oib1.mind_user_lc) in
   (* add  to avoid all indentifiers of lcstr1 *)
@@ -851,7 +851,7 @@ let mkProd_reldecl (rdecl:Context.Rel.Declaration.t) (t2:glob_constr) =
   match rdecl with
     | LocalAssum (nme,t) ->
         let t = EConstr.of_constr t in
-        let traw = Detyping.detype Detyping.Now false [] (Global.env()) Evd.empty t in
+        let traw = Detyping.detype Detyping.Now false Id.Set.empty (Global.env()) Evd.empty t in
         DAst.make @@ GProd (nme,Explicit,traw,t2)
     | LocalDef _ -> assert false
 
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index d43fd78f3..6fcfec80d 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -115,13 +115,17 @@ let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta
 (* Generic values *)
 let pf_get_new_ids idl g =
   let ids = pf_ids_of_hyps g in
+  let ids = Id.Set.of_list ids in
   List.fold_right
-    (fun id acc -> next_global_ident_away id (acc@ids)::acc)
+    (fun id acc -> next_global_ident_away id (Id.Set.union (Id.Set.of_list acc) ids)::acc)
     idl
     []
 
+let next_ident_away_in_goal ids avoid =
+  next_ident_away_in_goal ids (Id.Set.of_list avoid)
+
 let compute_renamed_type gls c =
-  rename_bound_vars_as_displayed (project gls) (*no avoid*) [] (*no rels*) []
+  rename_bound_vars_as_displayed (project gls) (*no avoid*) Id.Set.empty (*no rels*) []
     (pf_unsafe_type_of gls c)
 let h'_id = Id.of_string "h'"
 let teq_id = Id.of_string "teq"
@@ -1302,7 +1306,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
 	with e when CErrors.noncritical e ->
           anomaly (Pp.str "open_new_goal with an unamed theorem.")
   in
-  let na = next_global_ident_away name [] in
+  let na = next_global_ident_away name Id.Set.empty in
   if Termops.occur_existential sigma gls_type then
     CErrors.user_err Pp.(str "\"abstract\" cannot handle existentials");
   let hook _ _ =
diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index 4cab6ef33..be1d947d3 100644
--- a/plugins/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
@@ -88,7 +88,7 @@ let let_evar name typ =
     let id = match name with
     | Name.Anonymous ->
       let id = Namegen.id_of_name_using_hdchar env sigma typ name in
-      Namegen.next_ident_away_in_goal id (Termops.ids_of_named_context (Environ.named_context env))
+      Namegen.next_ident_away_in_goal id (Context.Named.to_vars (Environ.named_context env))
     | Name.Name id -> id
     in
     let (sigma, evar) = Evarutil.new_evar env sigma ~src ~naming:(Misctypes.IntroFresh id) typ in
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index b4c6f9c90..a7aebf9e1 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -665,7 +665,7 @@ let hResolve id c occ t =
   let sigma = Proofview.Goal.sigma gl in
   let env = Termops.clear_named_body id (Proofview.Goal.env gl) in
   let concl = Proofview.Goal.concl gl in
-  let env_ids = Termops.ids_of_context env in
+  let env_ids = Termops.vars_of_env env in
   let c_raw = Detyping.detype Detyping.Now true env_ids env sigma c in
   let t_raw = Detyping.detype Detyping.Now true env_ids env sigma t in
   let rec resolve_hole t_hole =
@@ -764,7 +764,7 @@ let case_eq_intros_rewrite x =
       mkCaseEq x;
     Proofview.Goal.enter begin fun gl ->
       let concl = Proofview.Goal.concl gl in
-      let hyps = Tacmach.New.pf_ids_of_hyps gl in
+      let hyps = Tacmach.New.pf_ids_set_of_hyps gl in
       let n' = nb_prod (Tacmach.New.project gl) concl in
       let h = fresh_id_in_env hyps (Id.of_string "heq") (Proofview.Goal.env gl)  in
       Tacticals.New.tclTHENLIST [
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index f4e3ba633..8a0764975 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -662,14 +662,14 @@ type 'a extra_genarg_printer =
         let names =
           List.fold_left
             (fun ln (nal,_) -> List.fold_left
-              (fun ln na -> match na with (_,Name id) -> id::ln | _ -> ln)
+              (fun ln na -> match na with (_,Name id) -> Id.Set.add id ln | _ -> ln)
               ln nal)
-            [] bll in
+            Id.Set.empty bll in
         let idarg,bll = set_nth_name names n bll in
-        let annot = match names with
-          | [_] ->
+        let annot =
+          if Int.equal (Id.Set.cardinal names) 1 then
             mt ()
-          | _ ->
+          else
             spc() ++ str"{"
             ++ keyword "struct" ++ spc ()
             ++ pr_id idarg ++ str"}"
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 3d01cbe8d..fd791a910 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -664,7 +664,7 @@ type rewrite_result =
 
 type 'a strategy_input = { state : 'a ; (* a parameter: for instance, a state *)
 			   env : Environ.env ;
-			   unfresh : Id.t list ; (* Unfresh names *)
+			   unfresh : Id.Set.t; (* Unfresh names *)
 			   term1 : constr ;
 			   ty1 : types ; (* first term and its type (convertible to rew_from) *)
 			   cstr : (bool (* prop *) * constr option) ;
@@ -1614,7 +1614,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
     in
     try
       let res =
-        cl_rewrite_clause_aux ?abs strat env [] sigma ty clause
+        cl_rewrite_clause_aux ?abs strat env Id.Set.empty sigma ty clause
       in
       let sigma = match origsigma with None -> sigma | Some sigma -> sigma in
       treat sigma res <*>
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index 23767c12f..63e891b45 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -110,7 +110,7 @@ val setoid_transitivity : constr option -> unit Proofview.tactic
 val apply_strategy :
   strategy ->
   Environ.env ->
-  Names.Id.t list ->
+  Names.Id.Set.t ->
   constr ->
   bool * constr ->
   evars -> rewrite_result
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 8fa95ffb0..18348bc11 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -139,7 +139,7 @@ let name_vfun appl vle =
 
 module TacStore = Geninterp.TacStore
 
-let f_avoid_ids : Id.t list TacStore.field = TacStore.field ()
+let f_avoid_ids : Id.Set.t TacStore.field = TacStore.field ()
 (* ids inherited from the call context (needed to get fresh ids) *)
 let f_debug : debug_info TacStore.field = TacStore.field ()
 let f_trace : ltac_trace TacStore.field = TacStore.field ()
@@ -501,29 +501,29 @@ let extract_ltac_constr_values ist env =
     could barely be defined as a feature... *)
 
 (* Extract the identifier list from lfun: join all branches (what to do else?)*)
-let rec intropattern_ids (loc,pat) = match pat with
-  | IntroNaming (IntroIdentifier id) -> [id]
+let rec intropattern_ids accu (loc,pat) = match pat with
+  | IntroNaming (IntroIdentifier id) -> Id.Set.add id accu
   | IntroAction (IntroOrAndPattern (IntroAndPattern l)) ->
-      List.flatten (List.map intropattern_ids l)
+      List.fold_left intropattern_ids accu l
   | IntroAction (IntroOrAndPattern (IntroOrPattern ll)) ->
-      List.flatten (List.map intropattern_ids (List.flatten ll))
+      List.fold_left intropattern_ids accu (List.flatten ll)
   | IntroAction (IntroInjection l) ->
-      List.flatten (List.map intropattern_ids l)
-  | IntroAction (IntroApplyOn ((_,c),pat)) -> intropattern_ids pat
+      List.fold_left intropattern_ids accu l
+  | IntroAction (IntroApplyOn ((_,c),pat)) -> intropattern_ids accu pat
   | IntroNaming (IntroAnonymous | IntroFresh _)
   | IntroAction (IntroWildcard | IntroRewrite _)
-  | IntroForthcoming _ -> []
+  | IntroForthcoming _ -> accu
 
-let extract_ids ids lfun =
+let extract_ids ids lfun accu =
   let fold id v accu =
     let v = Value.normalize v in
     if has_type v (topwit wit_intro_pattern) then
       let (_, ipat) = out_gen (topwit wit_intro_pattern) v in
       if Id.List.mem id ids then accu
-      else accu @ intropattern_ids (Loc.tag ipat)
+      else intropattern_ids accu (Loc.tag ipat)
     else accu
   in
-  Id.Map.fold fold lfun []
+  Id.Map.fold fold lfun accu
 
 let default_fresh_id = Id.of_string "H"
 
@@ -534,10 +534,10 @@ let interp_fresh_id ist env sigma l =
     with Not_found -> id in
   let ids = List.map_filter (function ArgVar (_, id) -> Some id | _ -> None) l in
   let avoid = match TacStore.get ist.extra f_avoid_ids with
-  | None -> []
+  | None -> Id.Set.empty
   | Some l -> l
   in
-  let avoid = (extract_ids ids ist.lfun) @ avoid in
+  let avoid = extract_ids ids ist.lfun avoid in
   let id =
     if List.is_empty l then default_fresh_id
     else
@@ -1303,7 +1303,7 @@ and interp_ltac_reference ?loc' mustbetac ist r : Val.t Ftactic.t =
       if mustbetac then Ftactic.return (coerce_to_tactic loc id v) else Ftactic.return v
       end
   | ArgArg (loc,r) ->
-      let ids = extract_ids [] ist.lfun in
+      let ids = extract_ids [] ist.lfun Id.Set.empty in
       let loc_info = (Option.default loc loc',LtacNameCall r) in
       let extra = TacStore.set ist.extra f_avoid_ids ids in
       push_trace loc_info ist >>= fun trace ->
@@ -1956,7 +1956,7 @@ let interp_tac_gen lfun avoid_ids debug t =
     (intern_pure_tactic { (Genintern.empty_glob_sign env) with ltacvars } t)
   end
 
-let interp t = interp_tac_gen Id.Map.empty [] (get_debug()) t
+let interp t = interp_tac_gen Id.Map.empty Id.Set.empty (get_debug()) t
 
 (* Used to hide interpretation for pretty-print, now just launch tactics *)
 (* [global] means that [t] should be internalized outside of goals. *)
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index c1ab2b4c4..d0a0a81d4 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -40,7 +40,7 @@ type interp_sign = Geninterp.interp_sign = {
   lfun : value Id.Map.t;
   extra : TacStore.t }
 
-val f_avoid_ids : Id.t list TacStore.field
+val f_avoid_ids : Id.Set.t TacStore.field
 val f_debug : debug_info TacStore.field
 
 val extract_ltac_constr_values : interp_sign -> Environ.env ->
@@ -113,7 +113,7 @@ val tactic_of_value : interp_sign -> Value.t -> unit Proofview.tactic
 
 (** Globalization + interpretation *)
 
-val interp_tac_gen : value Id.Map.t -> Id.t list ->
+val interp_tac_gen : value Id.Map.t -> Id.Set.t ->
                  debug_info -> raw_tactic_expr -> unit Proofview.tactic
 
 val interp : raw_tactic_expr -> unit Proofview.tactic
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index a4103634e..fc6781b06 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -1986,7 +1986,7 @@ let micromega_gen
        let intro_vars = Tacticals.New.tclTHENLIST (List.map intro vars) in
        let intro_props = Tacticals.New.tclTHENLIST (List.map intro props) in
        let ipat_of_name id = Some (Loc.tag @@ Misctypes.IntroNaming (Misctypes.IntroIdentifier id)) in
-       let goal_name = fresh_id [] (Names.Id.of_string "__arith") gl in
+       let goal_name = fresh_id Id.Set.empty (Names.Id.of_string "__arith") gl in
        let env' = List.map (fun (id,i) -> EConstr.mkVar id,i) vars in 
 
        let tac_arith = Tacticals.New.tclTHENLIST [ intro_props ; intro_vars ; 
@@ -2101,7 +2101,7 @@ let micromega_genr prover tac =
        let intro_vars = Tacticals.New.tclTHENLIST (List.map intro vars) in
        let intro_props = Tacticals.New.tclTHENLIST (List.map intro props) in
        let ipat_of_name id = Some (Loc.tag @@ Misctypes.IntroNaming (Misctypes.IntroIdentifier id)) in
-       let goal_name = fresh_id [] (Names.Id.of_string "__arith") gl in
+       let goal_name = fresh_id Id.Set.empty (Names.Id.of_string "__arith") gl in
        let env' = List.map (fun (id,i) -> EConstr.mkVar id,i) vars in 
        
        let tac_arith = Tacticals.New.tclTHENLIST [ intro_props ; intro_vars ; 
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 99493d698..ae1a563be 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -1760,7 +1760,7 @@ let onClearedName id tac =
   tclTHEN
     (tclTRY (clear [id]))
     (Proofview.Goal.nf_enter begin fun gl ->
-     let id = fresh_id [] id gl in
+     let id = fresh_id Id.Set.empty id gl in
      tclTHEN (introduction id) (tac id)
     end)
 
@@ -1768,8 +1768,8 @@ let onClearedName2 id tac =
   tclTHEN
     (tclTRY (clear [id]))
     (Proofview.Goal.nf_enter begin fun gl ->
-     let id1 = fresh_id [] (add_suffix id "_left") gl in
-     let id2 = fresh_id [] (add_suffix id "_right") gl in
+     let id1 = fresh_id Id.Set.empty (add_suffix id "_left") gl in
+     let id2 = fresh_id Id.Set.empty (add_suffix id "_right") gl in
       tclTHENLIST [ introduction id1; introduction id2; tac id1 id2 ]
     end)
 
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 8b69c3435..95ca6f49a 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -129,7 +129,7 @@ let newssrcongrtac arg ist gl =
     let eq, gl = pf_fresh_global (Coqlib.build_coq_eq ()) gl in
     pf_saturate gl (EConstr.of_constr eq) 3 in
   tclMATCH_GOAL (equality, gl') (fun gl' -> fs gl' (List.assoc 0 eq_args))
-  (fun ty -> congrtac (arg, Detyping.detype Detyping.Now false [] (pf_env gl) (project gl) ty) ist)
+  (fun ty -> congrtac (arg, Detyping.detype Detyping.Now false Id.Set.empty (pf_env gl) (project gl) ty) ist)
   (fun () ->
     let lhs, gl' = mk_evar gl EConstr.mkProp in let rhs, gl' = mk_evar gl' EConstr.mkProp in
     let arrow = EConstr.mkArrow lhs (EConstr.Vars.lift 1 rhs) in
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index 060225dab..1e1a986da 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -342,7 +342,7 @@ let interp_index ist gl idx =
         | None ->
         begin match Tacinterp.Value.to_constr v with
         | Some c ->
-          let rc = Detyping.detype Detyping.Now false [] (pf_env gl) (project gl) c in
+          let rc = Detyping.detype Detyping.Now false Id.Set.empty (pf_env gl) (project gl) c in
           begin match Notation.uninterp_prim_token rc with
           | _, Constrexpr.Numeral (s,b) ->
              let n = int_of_string s in if b then n else -n
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 7455587c0..af28e2a6b 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -113,8 +113,8 @@ let rec relocate_index sigma n1 n2 k t =
 
 type 'a rhs =
     { rhs_env    : env;
-      rhs_vars   : Id.t list;
-      avoid_ids  : Id.t list;
+      rhs_vars   : Id.Set.t;
+      avoid_ids  : Id.Set.t;
       it         : 'a option}
 
 type 'a equation =
@@ -553,7 +553,7 @@ let extract_rhs pb =
 let occur_in_rhs na rhs =
   match na with
     | Anonymous -> false
-    | Name id -> Id.List.mem id rhs.rhs_vars
+    | Name id -> Id.Set.mem id rhs.rhs_vars
 
 let is_dep_patt_in eqn pat = match DAst.get pat with
   | PatVar name -> Flags.is_program_mode () || occur_in_rhs name eqn.rhs
@@ -747,8 +747,8 @@ let get_names env sigma sign eqns =
   (* Otherwise, we take names from the parameters of the constructor but
      avoiding conflicts with user ids *)
   let allvars =
-    List.fold_left (fun l (_,_,eqn) -> List.union Id.equal l eqn.rhs.avoid_ids)
-      [] eqns in
+    List.fold_left (fun l (_,_,eqn) -> Id.Set.union l eqn.rhs.avoid_ids)
+      Id.Set.empty eqns in
   let names3,_ =
     List.fold_left2
       (fun (l,avoid) d na ->
@@ -757,7 +757,7 @@ let get_names env sigma sign eqns =
 	     (fun (LocalAssum (na,t) | LocalDef (na,_,t)) -> Name (next_name_away (named_hd env sigma t na) avoid))
 	     d na
 	 in
-         (na::l,(Name.get_id na)::avoid))
+         (na::l,Id.Set.add (Name.get_id na) avoid))
       ([],allvars) (List.rev sign) names2 in
   names3,aliasname
 
@@ -999,8 +999,8 @@ let add_assert_false_case pb tomatch =
   in
   [ { patterns = pats;
       rhs = { rhs_env = pb.env;
-	      rhs_vars = [];
-	      avoid_ids = [];
+	      rhs_vars = Id.Set.empty;
+	      avoid_ids = Id.Set.empty;
 	      it = None };
       alias_stack = Anonymous::aliasnames;
       eqn_loc = None;
@@ -1570,10 +1570,12 @@ let matx_of_eqns env eqns =
   let build_eqn (loc,(ids,lpat,rhs)) =
     let initial_lpat,initial_rhs = lpat,rhs in
     let initial_rhs = rhs in
+    let avoid = Context.Named.to_vars (named_context env) in
+    let avoid = List.fold_left (fun accu id -> Id.Set.add id accu) avoid ids in
     let rhs =
       { rhs_env = env;
         rhs_vars = free_glob_vars initial_rhs;
-	avoid_ids = ids@(ids_of_named_context (named_context env));
+	avoid_ids = avoid;
 	it = Some initial_rhs } in
     { patterns = initial_lpat;
       alias_stack = [];
@@ -1751,7 +1753,7 @@ let build_tycon ?loc env tycon_env s subst tycon extenv evdref t =
 let build_inversion_problem loc env sigma tms t =
   let make_patvar t (subst,avoid) =
     let id = next_name_away (named_hd env sigma t Anonymous) avoid in
-    DAst.make @@ PatVar (Name id), ((id,t)::subst, id::avoid) in
+    DAst.make @@ PatVar (Name id), ((id,t)::subst, Id.Set.add id avoid) in
   let rec reveal_pattern t (subst,avoid as acc) =
     match EConstr.kind sigma (whd_all env sigma t) with
     | Construct (cstr,u) -> DAst.make (PatCstr (cstr,[],Anonymous)), acc
@@ -1781,7 +1783,7 @@ let build_inversion_problem loc env sigma tms t =
       let d = LocalAssum (alias_of_pat pat,typ) in
       let patl,acc_sign,acc = aux (n+1) (push_rel d env) (d::acc_sign) tms acc in
       pat::patl,acc_sign,acc in
-  let avoid0 = ids_of_context env in
+  let avoid0 = vars_of_env env in
   (* [patl] is a list of patterns revealing the substructure of
      constructors present in the constraints on the type of the
      multiple terms t1..tn that are matched in the original problem;
@@ -1823,7 +1825,7 @@ let build_inversion_problem loc env sigma tms t =
       rhs = { rhs_env = pb_env;
               (* we assume all vars are used; in practice we discard dependent
 		 vars so that the field rhs_vars is normally not used *)
-              rhs_vars = List.map fst subst;
+              rhs_vars = List.fold_left (fun accu (id, _) -> Id.Set.add id accu) Id.Set.empty subst;
               avoid_ids = avoid;
 	      it = Some (lift n t) } } in
   (* [catch_all] is a catch-all default clause of the auxiliary
@@ -1841,7 +1843,7 @@ let build_inversion_problem loc env sigma tms t =
           eqn_loc = None;
           used = ref false;
           rhs = { rhs_env = pb_env;
-                  rhs_vars = [];
+                  rhs_vars = Id.Set.empty;
 	          avoid_ids = avoid0;
 	          it = None } } ] in
   (* [pb] is the auxiliary pattern-matching serving as skeleton for the
@@ -2085,7 +2087,7 @@ let prime avoid name =
 
 let make_prime avoid prevname =
   let previd, id = prime !avoid prevname in
-    avoid := id :: !avoid;
+    avoid := Id.Set.add id !avoid;
     previd, id
 
 let eq_id avoid id =
@@ -2113,7 +2115,7 @@ let constr_of_pat env evdref arsign pat avoid =
 	    Name n -> name, avoid
 	  | Anonymous ->
 	      let previd, id = prime avoid (Name (Id.of_string "wildcard")) in
-		Name id, id :: avoid
+		Name id, Id.Set.add id avoid
 	in
 	  ((DAst.make ?loc @@ PatVar name), [LocalAssum (name, ty)] @ realargs, mkRel 1, ty,
 	   (List.map (fun x -> mkRel 1) realargs), 1, avoid)
@@ -2157,7 +2159,7 @@ let constr_of_pat env evdref arsign pat avoid =
 		pat', sign, app, apptype, realargs, n, avoid
 	    | Name id ->
 		let sign = LocalAssum (alias, lift m ty) :: sign in
-		let avoid = id :: avoid in
+		let avoid = Id.Set.add id avoid in
 		let sign, i, avoid =
 		  try
 		    let env = push_rel_context sign env in
@@ -2168,7 +2170,7 @@ let constr_of_pat env evdref arsign pat avoid =
 		      (lift 1 app) (* aliased term *)
 		    in
 		    let neq = eq_id avoid id in
-		      LocalDef (Name neq, mkRel 0, eq_t) :: sign, 2, neq :: avoid
+		      LocalDef (Name neq, mkRel 0, eq_t) :: sign, 2, Id.Set.add neq avoid
 		  with Reduction.NotConvertible -> sign, 1, avoid
 		in
 		  (* Mark the equality as a hole *)
@@ -2182,7 +2184,7 @@ let constr_of_pat env evdref arsign pat avoid =
 let eq_id avoid id =
   let hid = Id.of_string ("Heq_" ^ Id.to_string id) in
   let hid' = next_ident_away hid !avoid in
-    avoid := hid' :: !avoid;
+    avoid := Id.Set.add hid' !avoid;
     hid'
 
 let is_topvar sigma t =
@@ -2278,7 +2280,7 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity =
 	     (fun (idents, newpatterns, pats) pat arsign ->
 		let pat', cpat, idents = constr_of_pat env evdref arsign pat idents in
 		  (idents, pat' :: newpatterns, cpat :: pats))
-	      ([], [], []) eqn.patterns sign
+	      (Id.Set.empty, [], []) eqn.patterns sign
 	 in
 	 let newpatterns = List.rev newpatterns and opats = List.rev pats in
 	 let rhs_rels, pats, signlen =
@@ -2379,8 +2381,8 @@ let abstract_tomatch env sigma tomatchs tycon =
 	       let name = next_ident_away (Id.of_string "filtered_var") names in
 		 (mkRel 1, lift_tomatch_type (succ lenctx) t) :: lift_ctx 1 prev,
 	       LocalDef (Name name, lift lenctx c, lift lenctx $ type_of_tomatch t) :: ctx,
-	       name :: names, tycon)
-      ([], [], [], tycon) tomatchs
+	       Id.Set.add name names, tycon)
+      ([], [], Id.Set.empty, tycon) tomatchs
   in List.rev prev, ctx, tycon
 
 let build_dependent_signature env evdref avoid tomatchs arsign =
@@ -2502,7 +2504,7 @@ let compile_program_cases ?loc style (typing_function, evdref) tycon env lvar
     let arsign = List.map fst arsign in (* Because no difference between the arity for typing and the arity for building *)
       (* Build the dependent arity signature, the equalities which makes
 	 the first part of the predicate and their instantiations. *)
-    let avoid = [] in
+    let avoid = Id.Set.empty in
       build_dependent_signature env evdref avoid tomatchs arsign
 
   in
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 428f64b99..7bdc604b8 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -49,16 +49,16 @@ val constr_of_pat :
            Evd.evar_map ref ->
            rel_context ->
            Glob_term.cases_pattern ->
-           Names.Id.t list ->
+           Names.Id.Set.t ->
            Glob_term.cases_pattern *
            (rel_context * constr *
             (types * constr list) * Glob_term.cases_pattern) *
-           Names.Id.t list
+           Names.Id.Set.t
 
 type 'a rhs =
     { rhs_env    : env;
-      rhs_vars   : Id.t list;
-      avoid_ids  : Id.t list;
+      rhs_vars   : Id.Set.t;
+      avoid_ids  : Id.Set.t;
       it         : 'a option}
 
 type 'a equation =
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index fc0a650bc..7cfd2e27d 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -205,7 +205,7 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr)
 	| _ -> subco ())
       | Prod (name, a, b), Prod (name', a', b') ->
 	  let name' = 
-	    Name (Namegen.next_ident_away Namegen.default_dependent_ident (Termops.ids_of_context env))
+	    Name (Namegen.next_ident_away Namegen.default_dependent_ident (Termops.vars_of_env env))
 	  in
 	  let env' = push_rel (LocalAssum (name', a')) env in
 	  let c1 = coerce_unify env' (lift 1 a') (lift 1 a) in
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index ca7f633dc..0973d73ee 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -178,7 +178,7 @@ let push_binder na1 na2 t ctx =
   let id2 = match na2 with
   | Name id2 -> id2
   | Anonymous ->
-     let avoid = List.map pi2 ctx in
+     let avoid = Id.Set.of_list (List.map pi2 ctx) in
      Namegen.next_ident_away Namegen.default_non_dependent_ident avoid in
   (na1, id2, t) :: ctx
 
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 5e1430741..d81b88660 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -221,12 +221,12 @@ let lookup_name_as_displayed env sigma t s =
 	   | (Anonymous,avoid') -> lookup avoid' (n+1) (pop c'))
     | Cast (c,_,_) -> lookup avoid n c
     | _ -> None
-  in lookup (ids_of_named_context (named_context env)) 1 t
+  in lookup (Context.Named.to_vars (named_context env)) 1 t
 
 let lookup_index_as_renamed env sigma t n =
   let rec lookup n d c = match EConstr.kind sigma c with
     | Prod (name,_,c') ->
-	  (match compute_displayed_name_in sigma RenamingForGoal [] name c' with
+	  (match compute_displayed_name_in sigma RenamingForGoal Id.Set.empty name c' with
                (Name _,_) -> lookup n (d+1) c'
              | (Anonymous,_) ->
 		 if Int.equal n 0 then
@@ -236,7 +236,7 @@ let lookup_index_as_renamed env sigma t n =
 		 else
 		   lookup (n-1) (d+1) c')
     | LetIn (name,_,_,c') ->
-	  (match compute_displayed_name_in sigma RenamingForGoal [] name c' with
+	  (match compute_displayed_name_in sigma RenamingForGoal Id.Set.empty name c' with
              | (Name _,_) -> lookup n (d+1) c'
              | (Anonymous,_) ->
 		 if Int.equal n 0 then
@@ -578,7 +578,7 @@ and detype_fix d flags avoid env sigma (vn,_ as nvn) (names,tys,bodies) =
     Array.fold_left2
       (fun (avoid, env, l) na ty ->
 	 let id = next_name_away na avoid in
-	 (id::avoid, add_name (Name id) None ty env, id::l))
+	 (Id.Set.add id avoid, add_name (Name id) None ty env, id::l))
       (avoid, env, []) names tys in
   let n = Array.length tys in
   let v = Array.map3
@@ -594,7 +594,7 @@ and detype_cofix d flags avoid env sigma n (names,tys,bodies) =
     Array.fold_left2
       (fun (avoid, env, l) na ty ->
 	 let id = next_name_away na avoid in
-	 (id::avoid, add_name (Name id) None ty env, id::l))
+	 (Id.Set.add id avoid, add_name (Name id) None ty env, id::l))
       (avoid, env, []) names tys in
   let ntys = Array.length tys in
   let v = Array.map2
@@ -615,14 +615,14 @@ and share_names d flags n l avoid env sigma c t =
           | _ -> na in
         let t' = detype d flags avoid env sigma t in
 	let id = next_name_away na avoid in
-        let avoid = id::avoid and env = add_name (Name id) None t env in
+        let avoid = Id.Set.add id avoid and env = add_name (Name id) None t env in
         share_names d flags (n-1) ((Name id,Explicit,None,t')::l) avoid env sigma c c'
     (* May occur for fix built interactively *)
     | LetIn (na,b,t',c), _ when n > 0 ->
         let t'' = detype d flags avoid env sigma t' in
         let b' = detype d flags avoid env sigma b in
 	let id = next_name_away na avoid in
-        let avoid = id::avoid and env = add_name (Name id) (Some b) t' env in
+        let avoid = Id.Set. add id avoid and env = add_name (Name id) (Some b) t' env in
         share_names d flags n ((Name id,Explicit,Some b',t'')::l) avoid env sigma c (lift 1 t)
     (* Only if built with the f/n notation or w/o let-expansion in types *)
     | _, LetIn (_,b,_,t) when n > 0 ->
@@ -631,7 +631,7 @@ and share_names d flags n l avoid env sigma c t =
     | _, Prod (na',t',c') when n > 0 ->
         let t'' = detype d flags avoid env sigma t' in
 	let id = next_name_away na' avoid in
-        let avoid = id::avoid and env = add_name (Name id) None t' env in
+        let avoid = Id.Set.add id avoid and env = add_name (Name id) None t' env in
         let appc = mkApp (lift 1 c,[|mkRel 1|]) in
         share_names d flags (n-1) ((Name id,Explicit,None,t'')::l) avoid env sigma appc c'
     (* If built with the f/n notation: we renounce to share names *)
@@ -822,7 +822,7 @@ let rec subst_glob_constr subst = DAst.map (function
   | GRef (ref,u) as raw ->
       let ref',t = subst_global subst ref in
 	if ref' == ref then raw else
-         DAst.get (detype Now false [] (Global.env()) Evd.empty (EConstr.of_constr t))
+         DAst.get (detype Now false Id.Set.empty (Global.env()) Evd.empty (EConstr.of_constr t))
 
   | GSort _
   | GVar _
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 67c852af3..b70bfd83c 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -35,16 +35,16 @@ val subst_glob_constr : substitution -> glob_constr -> glob_constr
    [isgoal] tells if naming must avoid global-level synonyms as intro does 
    [ctx] gives the names of the free variables *)
 
-val detype_names : bool -> Id.t list -> names_context -> env -> evar_map -> constr -> glob_constr
+val detype_names : bool -> Id.Set.t -> names_context -> env -> evar_map -> constr -> glob_constr
 
-val detype : 'a delay -> ?lax:bool -> bool -> Id.t list -> env -> evar_map -> constr -> 'a glob_constr_g
+val detype : 'a delay -> ?lax:bool -> bool -> Id.Set.t -> env -> evar_map -> constr -> 'a glob_constr_g
 
 val detype_sort : evar_map -> sorts -> glob_sort
 
-val detype_rel_context : 'a delay -> ?lax:bool -> constr option -> Id.t list -> (names_context * env) -> 
+val detype_rel_context : 'a delay -> ?lax:bool -> constr option -> Id.Set.t -> (names_context * env) -> 
   evar_map -> rel_context -> 'a glob_decl_g list
 
-val detype_closed_glob : ?lax:bool -> bool -> Id.t list -> env -> evar_map -> closed_glob_constr -> glob_constr
+val detype_closed_glob : ?lax:bool -> bool -> Id.Set.t -> env -> evar_map -> closed_glob_constr -> glob_constr
 
 (** look for the index of a named var or a nondep var as it is renamed *)
 val lookup_name_as_displayed  : env -> evar_map -> constr -> Id.t -> int option
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index 7f5a780f9..9fed28bb3 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -72,7 +72,7 @@ let define_pure_evar_as_product evd evk =
   let open Context.Named.Declaration in
   let evi = Evd.find_undefined evd evk in
   let evenv = evar_env evi in
-  let id = next_ident_away idx (ids_of_named_context (evar_context evi)) in
+  let id = next_ident_away idx (Context.Named.to_vars (evar_context evi)) in
   let concl = Reductionops.whd_all evenv evd (EConstr.of_constr evi.evar_concl) in
   let s = destSort evd concl in
   let evd1,(dom,u1) =
@@ -127,7 +127,7 @@ let define_pure_evar_as_lambda env evd evk =
   | Prod (na,dom,rng) -> (evd,(na,dom,rng))
   | Evar ev' -> let evd,typ = define_evar_as_product evd ev' in evd,destProd evd typ
   | _ -> error_not_product env evd typ in
-  let avoid = ids_of_named_context (evar_context evi) in
+  let avoid = Context.Named.to_vars (evar_context evi) in
   let id =
     next_name_away_with_default_using_types "x" na avoid (Reductionops.whd_evar evd dom) in
   let newenv = push_named (LocalAssum (id, dom)) evenv in
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index ef0fb8ea6..8652a4146 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -679,6 +679,7 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
   let filter1 = evar_filter evi1 in
   let src = subterm_source evk1 evi1.evar_source in
   let ids1 = List.map get_id (named_context_of_val sign1) in
+  let avoid = Context.Named.to_vars (named_context_of_val sign1) in
   let inst_in_sign = List.map mkVar (Filter.filter_list filter1 ids1) in
   let open Context.Rel.Declaration in
   let (sign2,filter2,inst2_in_env,inst2_in_sign,_,evd,_) =
@@ -700,9 +701,9 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
       (push_named_context_val d' sign, Filter.extend 1 filter,
        (mkRel 1)::(List.map (lift 1) inst_in_env),
        (mkRel 1)::(List.map (lift 1) inst_in_sign),
-       push_rel d env,evd,id::avoid))
+       push_rel d env,evd,Id.Set.add id avoid))
       rel_sign
-      (sign1,filter1,Array.to_list args1,inst_in_sign,env1,evd,ids1)
+      (sign1,filter1,Array.to_list args1,inst_in_sign,env1,evd,avoid)
   in
   let evd,ev2ty_in_sign =
     let s = Retyping.get_sort_of env evd ty_in_env in
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index e1576b971..7804cc679 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -273,17 +273,17 @@ let free_glob_vars =
     | _ -> fold_glob_constr_with_binders Id.Set.add vars bound vs c in
   fun rt ->
     let vs = vars Id.Set.empty Id.Set.empty rt in
-    Id.Set.elements vs
+    vs
 
 let glob_visible_short_qualid c =
   let rec aux acc c = match DAst.get c with
     | GRef (c,_) ->
         let qualid = Nametab.shortest_qualid_of_global Id.Set.empty c in
         let dir,id = Libnames.repr_qualid  qualid in
-        if DirPath.is_empty dir then id :: acc else acc
+        if DirPath.is_empty dir then Id.Set.add id acc else acc
     | _ ->
         fold_glob_constr aux acc c
-  in aux [] c
+  in aux Id.Set.empty c
 
 let warn_variable_collision =
   let open Pp in
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index bacc8fbe4..49ea9727c 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -43,11 +43,11 @@ val fold_glob_constr : ('a -> glob_constr -> 'a) -> 'a -> glob_constr -> 'a
 val fold_glob_constr_with_binders : (Id.t -> 'a -> 'a) -> ('a -> 'b -> glob_constr -> 'b) -> 'a -> 'b -> glob_constr -> 'b
 val iter_glob_constr : (glob_constr -> unit) -> glob_constr -> unit
 val occur_glob_constr : Id.t -> 'a glob_constr_g -> bool
-val free_glob_vars : 'a glob_constr_g -> Id.t list
+val free_glob_vars : 'a glob_constr_g -> Id.Set.t
 val bound_glob_vars : glob_constr -> Id.Set.t
 (* Obsolete *)
 val loc_of_glob_constr : 'a glob_constr_g -> Loc.t option
-val glob_visible_short_qualid : 'a glob_constr_g -> Id.t list
+val glob_visible_short_qualid : 'a glob_constr_g -> Id.Set.t
 
 (* Renaming free variables using a renaming map; fails with
    [UnsoundRenaming] if applying the renaming would introduce
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index f090921e5..59cb43302 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1616,7 +1616,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
   let id =
     let t = match ty with Some t -> t | None -> get_type_of env sigma c in
     let x = id_of_name_using_hdchar (Global.env()) sigma t name in
-    let ids = ids_of_named_context (named_context env) in
+    let ids = Context.Named.to_vars (named_context env) in
     if name == Anonymous then next_ident_away_in_goal x ids else
     if mem_named_context_val x (named_context_val env) then
       user_err ~hdr:"Unification.make_abstraction_core"
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 219eafda4..755e905a7 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -64,9 +64,10 @@ let get_new_id locals id =
       if not (Nametab.exists_module dir) then
 	id
       else
-	get_id (id::l) (Namegen.next_ident_away id l)
+	get_id (Id.Set.add id l) (Namegen.next_ident_away id l)
   in
-    get_id (List.map snd locals) id
+  let avoid = List.fold_left (fun accu (_, id) -> Id.Set.add id accu) Id.Set.empty locals in
+    get_id avoid id
 
 (** Inductive declarations *)
 
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index ea60be31f..5ef7fac81 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -557,7 +557,7 @@ let make_clenv_binding_gen hyps_only n env sigma (c,t) = function
       let clause = mk_clenv_from_env env sigma n (c,t) in
       clenv_constrain_dep_args hyps_only largs clause
   | ExplicitBindings lbind ->
-      let t = rename_bound_vars_as_displayed sigma [] [] t in
+      let t = rename_bound_vars_as_displayed sigma Id.Set.empty [] t in
       let clause = mk_clenv_from_env env sigma n
 	(c, t)
       in clenv_match_args lbind clause
@@ -605,7 +605,7 @@ let make_evar_clause env sigma ?len t =
   | Some n -> assert (0 <= n); n
   in
   (** FIXME: do the renaming online *)
-  let t = rename_bound_vars_as_displayed sigma [] [] t in
+  let t = rename_bound_vars_as_displayed sigma Id.Set.empty [] t in
   let rec clrec (sigma, holes) n t =
     if n = 0 then (sigma, holes, t)
     else match EConstr.kind sigma t with
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index a4d662e0a..b08051d75 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -64,15 +64,10 @@ let pf_get_hyp_typ gls id =
   id |> pf_get_hyp gls |> NamedDecl.get_type
 
 let pf_ids_of_hyps gls = ids_of_named_context (pf_hyps gls)
+let pf_ids_set_of_hyps gls = Context.Named.to_vars (pf_hyps gls)
 
 let pf_get_new_id id gls =
-  next_ident_away id (pf_ids_of_hyps gls)
-
-let pf_get_new_ids ids gls =
-  let avoid = pf_ids_of_hyps gls in
-  List.fold_right
-    (fun id acc -> (next_ident_away id (acc@avoid))::acc)
-    ids []
+  next_ident_away id (pf_ids_set_of_hyps gls)
 
 let pf_global gls id = EConstr.of_constr (Universes.constr_of_global (Constrintern.construct_reference (pf_hyps gls) id))
 
@@ -177,8 +172,14 @@ module New = struct
     let hyps = Proofview.Goal.hyps gl in
     ids_of_named_context hyps
 
+  let pf_ids_set_of_hyps gl =
+    (** We only get the identifiers in [hyps] *)
+    let gl = Proofview.Goal.assume gl in
+    let hyps = Proofview.Goal.hyps gl in
+    Context.Named.to_vars hyps
+
   let pf_get_new_id id gl =
-    let ids = pf_ids_of_hyps gl in
+    let ids = pf_ids_set_of_hyps gl in
     next_ident_away id ids
 
   let pf_get_hyp id gl =
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 93bf428fd..7e6d83b10 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -48,7 +48,6 @@ val pf_get_hyp            : goal sigma -> Id.t -> named_declaration
 val pf_get_hyp_typ        : goal sigma -> Id.t -> types
 
 val pf_get_new_id  : Id.t      -> goal sigma -> Id.t
-val pf_get_new_ids : Id.t list -> goal sigma -> Id.t list
 
 val pf_reduction_of_red_expr : goal sigma -> red_expr -> constr -> evar_map * constr
 
@@ -120,6 +119,7 @@ module New : sig
 
   val pf_get_new_id  : identifier -> 'a Proofview.Goal.t -> identifier
   val pf_ids_of_hyps : 'a Proofview.Goal.t -> identifier list
+  val pf_ids_set_of_hyps : 'a Proofview.Goal.t -> Id.Set.t
   val pf_hyps_types : 'a Proofview.Goal.t -> (identifier * types) list
 
   val pf_get_hyp : identifier -> 'a Proofview.Goal.t -> named_declaration
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index e16fcec7c..d912decff 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -73,7 +73,7 @@ let generalize_right mk typ c1 c2 =
     let env = Proofview.Goal.env gl in
     let store = Proofview.Goal.extra gl in
   Refine.refine ~typecheck:false begin fun sigma ->
-    let na = Name (next_name_away_with_default "x" Anonymous (Termops.ids_of_context env)) in
+    let na = Name (next_name_away_with_default "x" Anonymous (Termops.vars_of_env env)) in
     let newconcl = mkProd (na, typ, mk typ c1 (mkRel 1)) in
     let (sigma, x) = Evarutil.new_evar env sigma ~principal:true ~store newconcl in
     (sigma, mkApp (x, [|c2|]))
@@ -114,7 +114,7 @@ let idx = Id.of_string "x"
 let idy = Id.of_string "y"
 
 let mkGenDecideEqGoal rectype ops g =
-  let hypnames = pf_ids_of_hyps g in
+  let hypnames = pf_ids_set_of_hyps g in
   let xname    = next_ident_away idx hypnames
   and yname    = next_ident_away idy hypnames in
   (mkNamedProd xname rectype
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index ce57682c6..bfbac7787 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -64,7 +64,7 @@ module RelDecl = Context.Rel.Declaration
 let hid = Id.of_string "H"
 let xid = Id.of_string "X"
 let default_id_of_sort = function InProp | InSet -> hid | InType -> xid
-let fresh env id = next_global_ident_away id []
+let fresh env id = next_global_ident_away id Id.Set.empty
 let with_context_set ctx (b, ctx') = 
   (b, Univ.ContextSet.union ctx ctx')
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 3ea9538f3..e33dd2e5e 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1003,7 +1003,7 @@ let apply_on_clause (f,t) clause =
 let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn =
   build_coq_True () >>= fun true_0 ->
   build_coq_False () >>= fun false_0 ->
-  let e = next_ident_away eq_baseid (ids_of_context env) in
+  let e = next_ident_away eq_baseid (vars_of_env env) in
   let e_env = push_named (Context.Named.Declaration.LocalAssum (e,t)) env in
   let discriminator =
     try
@@ -1371,7 +1371,7 @@ let simplify_args env sigma t =
     | _ -> t
 
 let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
-  let e = next_ident_away eq_baseid (ids_of_context env) in
+  let e = next_ident_away eq_baseid (vars_of_env env) in
   let e_env = push_named (LocalAssum (e,t)) env in
   let evdref = ref sigma in
   let filter (cpath, t1', t2') =
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 9495ca9c5..f391382bf 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -387,7 +387,7 @@ let rewrite_equations as_mode othin neqns names ba =
   Proofview.Goal.enter begin fun gl ->
   let (depids,nodepids) = split_dep_and_nodep ba.Tacticals.assums gl in
   let first_eq = ref MoveLast in
-  let avoid = if as_mode then List.map NamedDecl.get_id nodepids else [] in
+  let avoid = if as_mode then Id.Set.of_list (List.map NamedDecl.get_id nodepids) else Id.Set.empty in
   match othin with
     | Some thin ->
         tclTHENLIST
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 7c488f524..cc9d98f6f 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -142,7 +142,7 @@ let rec add_prods_sign env sigma t =
 
 let compute_first_inversion_scheme env sigma ind sort dep_option =
   let indf,realargs = dest_ind_type ind in
-  let allvars = ids_of_context env in
+  let allvars = vars_of_env env in
   let p = next_ident_away (Id.of_string "P") allvars in
   let pty,goal =
     if dep_option  then
@@ -214,7 +214,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
 	 else Context.Named.add d sign)
       invEnv ~init:Context.Named.empty
   end in
-  let avoid = ref [] in
+  let avoid = ref Id.Set.empty in
   let { sigma=sigma } = Proof.V82.subgoals pf in
   let sigma = Evd.nf_constraints sigma in
   let rec fill_holes c =
@@ -222,7 +222,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
     | Evar (e,args) ->
 	let h = next_ident_away (Id.of_string "H") !avoid in
 	let ty,inst = Evarutil.generalize_evar_over_rels sigma (e,args) in
-	avoid := h::!avoid;
+	avoid := Id.Set.add h !avoid;
 	ownSign := Context.Named.add (LocalAssum (h,ty)) !ownSign;
 	applist (mkVar h, inst)
     | _ -> EConstr.map sigma fill_holes c
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f1dd61358..4a0525889 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -384,7 +384,7 @@ let rename_hyp repl =
 (**************************************************************)
 
 let fresh_id_in_env avoid id env =
-  next_ident_away_in_goal id (avoid@ids_of_named_context (named_context env))
+  next_ident_away_in_goal id (Id.Set.union avoid (Context.Named.to_vars (named_context env)))
 
 let fresh_id avoid id gl =
   fresh_id_in_env avoid id (pf_env gl)
@@ -412,12 +412,12 @@ let default_id env sigma decl =
    possibly a move to do after the introduction *)
 
 type name_flag =
-  | NamingAvoid of Id.t list
-  | NamingBasedOn of Id.t * Id.t list
+  | NamingAvoid of Id.Set.t
+  | NamingBasedOn of Id.t * Id.Set.t
   | NamingMustBe of Id.t Loc.located
 
 let naming_of_name = function
-  | Anonymous -> NamingAvoid []
+  | Anonymous -> NamingAvoid Id.Set.empty
   | Name id -> NamingMustBe (Loc.tag id)
 
 let find_name mayrepl decl naming gl = match naming with
@@ -429,7 +429,7 @@ let find_name mayrepl decl naming gl = match naming with
   | NamingBasedOn (id,idl) ->  new_fresh_id idl id gl
   | NamingMustBe (loc,id) ->
       (* When name is given, we allow to hide a global name *)
-      let ids_of_hyps = Tacmach.New.pf_ids_of_hyps gl in
+      let ids_of_hyps = Tacmach.New.pf_ids_set_of_hyps gl in
       let id' = next_ident_away id ids_of_hyps in
       if not mayrepl && not (Id.equal id' id) then
         user_err ?loc  (pr_id id ++ str" is already used.");
@@ -603,7 +603,7 @@ let fix ido n = match ido with
   | None ->
     Proofview.Goal.enter begin fun gl ->
       let name = Proof_global.get_current_proof_name () in
-      let id = new_fresh_id [] name gl in
+      let id = new_fresh_id Id.Set.empty name gl in
       mutual_fix id n [] 0
     end
   | Some id ->
@@ -654,7 +654,7 @@ let cofix ido = match ido with
   | None ->
     Proofview.Goal.enter begin fun gl ->
       let name = Proof_global.get_current_proof_name () in
-      let id = new_fresh_id [] name gl in
+      let id = new_fresh_id Id.Set.empty name gl in
       mutual_cofix id [] 0
     end
   | Some id ->
@@ -975,13 +975,13 @@ let unfold_constr = function
    the type to build hyp names, we maintain an environment to be able
    to type dependent hyps. *)
 let find_intro_names ctxt gl =
-  let _, res = List.fold_right
+  let _, res, _ = List.fold_right
     (fun decl acc ->
-      let env,idl = acc in
-      let name = fresh_id idl (default_id env gl.sigma decl) gl in
+      let env,idl,avoid = acc in
+      let name = fresh_id avoid (default_id env gl.sigma decl) gl in
       let newenv = push_rel decl env in
-      (newenv,(name::idl)))
-    ctxt (pf_env gl , []) in
+      (newenv, name :: idl, Id.Set.add name avoid))
+    ctxt (pf_env gl, [], Id.Set.empty) in
   List.rev res
 
 let build_intro_tac id dest tac = match dest with
@@ -1021,18 +1021,18 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac =
 
 let intro_gen n m f d = intro_then_gen n m f d (fun _ -> Proofview.tclUNIT ())
 let intro_mustbe_force id = intro_gen (NamingMustBe (Loc.tag id)) MoveLast true false
-let intro_using id = intro_gen (NamingBasedOn (id,[])) MoveLast false false
+let intro_using id = intro_gen (NamingBasedOn (id, Id.Set.empty)) MoveLast false false
 
-let intro_then = intro_then_gen (NamingAvoid []) MoveLast false false
-let intro = intro_gen (NamingAvoid []) MoveLast false false
-let introf = intro_gen (NamingAvoid []) MoveLast true false
+let intro_then = intro_then_gen (NamingAvoid Id.Set.empty) MoveLast false false
+let intro = intro_gen (NamingAvoid Id.Set.empty) MoveLast false false
+let introf = intro_gen (NamingAvoid Id.Set.empty) MoveLast true false
 let intro_avoiding l = intro_gen (NamingAvoid l) MoveLast false false
 
 let intro_move_avoid idopt avoid hto = match idopt with
   | None -> intro_gen (NamingAvoid avoid) hto true false
   | Some id -> intro_gen (NamingMustBe (Loc.tag id)) hto true false
 
-let intro_move idopt hto = intro_move_avoid idopt [] hto
+let intro_move idopt hto = intro_move_avoid idopt Id.Set.empty hto
 
 (**** Multiple introduction tactics ****)
 
@@ -1264,7 +1264,7 @@ let cut c =
       with e when Pretype_errors.precatchable_exception e -> false
     in
     if is_sort then
-      let id = next_name_away_with_default "H" Anonymous (Tacmach.New.pf_ids_of_hyps gl) in
+      let id = next_name_away_with_default "H" Anonymous (Tacmach.New.pf_ids_set_of_hyps gl) in
       (** Backward compat: normalize [c]. *)
       let c = if normalize_cut then local_strong whd_betaiota sigma c else c in
       Refine.refine ~typecheck:false begin fun h ->
@@ -1763,7 +1763,7 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind :
         let info = Option.cata (fun loc -> Loc.add_loc info loc) info loc in
         let tac =
           if with_destruct then
-            descend_in_conjunctions []
+            descend_in_conjunctions Id.Set.empty
               (fun b id ->
                 Tacticals.New.tclTHEN
                   (try_main_apply b (mkVar id))
@@ -1912,7 +1912,7 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming
           ])
     with e when with_destruct && CErrors.noncritical e ->
       let (e, info) = CErrors.push e in
-        (descend_in_conjunctions [targetid]
+        (descend_in_conjunctions (Id.Set.singleton targetid)
            (fun b id -> aux (id::idstoclear) b (mkVar id))
            (e, info) c)
     end
@@ -2392,15 +2392,16 @@ let rewrite_hyp_then assert_style with_evars thin l2r id tac =
 
 let prepare_naming ?loc = function
   | IntroIdentifier id -> NamingMustBe (Loc.tag ?loc id)
-  | IntroAnonymous -> NamingAvoid []
-  | IntroFresh id -> NamingBasedOn (id,[])
+  | IntroAnonymous -> NamingAvoid Id.Set.empty
+  | IntroFresh id -> NamingBasedOn (id, Id.Set.empty)
 
 let rec explicit_intro_names = function
 | (_, IntroForthcoming _) :: l -> explicit_intro_names l
-| (_, IntroNaming (IntroIdentifier id)) :: l -> id :: explicit_intro_names l
+| (_, IntroNaming (IntroIdentifier id)) :: l -> Id.Set.add id (explicit_intro_names l)
 | (_, IntroAction (IntroOrAndPattern l)) :: l' ->
     let ll = match l with IntroAndPattern l -> [l] | IntroOrPattern ll -> ll in
-    List.flatten (List.map (fun l -> explicit_intro_names (l@l')) ll)
+    let fold accu l = Id.Set.union accu (explicit_intro_names (l@l')) in
+    List.fold_left fold Id.Set.empty ll
 | (_, IntroAction (IntroInjection l)) :: l' ->
     explicit_intro_names (l@l')
 | (_, IntroAction (IntroApplyOn (c,pat))) :: l' ->
@@ -2408,7 +2409,7 @@ let rec explicit_intro_names = function
 | (_, (IntroNaming (IntroAnonymous | IntroFresh _)
      | IntroAction (IntroWildcard | IntroRewrite _))) :: l ->
      explicit_intro_names l
-| [] -> []
+| [] -> Id.Set.empty
 
 let rec check_name_unicity env ok seen = function
 | (_, IntroForthcoming _) :: l -> check_name_unicity env ok seen l
@@ -2455,8 +2456,8 @@ let make_tmp_naming avoid l = function
      IntroAnonymous, but at the cost of a "renaming"; Note that in the
      case of IntroFresh, we should use check_thin_clash_then anyway to
      prevent the case of an IntroFresh precisely using the wild_id *)
-  | IntroWildcard -> NamingBasedOn (wild_id,avoid@explicit_intro_names l)
-  | pat -> NamingAvoid(avoid@explicit_intro_names ((Loc.tag @@ IntroAction pat)::l))
+  | IntroWildcard -> NamingBasedOn (wild_id, Id.Set.union avoid (explicit_intro_names l))
+  | pat -> NamingAvoid(Id.Set.union avoid (explicit_intro_names ((Loc.tag @@ IntroAction pat)::l)))
 
 let fit_bound n = function
   | None -> true
@@ -2497,7 +2498,7 @@ let rec intro_patterns_core with_evars b avoid ids thin destopt bound n tac =
   if exceed_bound n bound then error_unexpected_extra_pattern loc bound pat else
   match pat with
   | IntroForthcoming onlydeps ->
-      intro_forthcoming_then_gen (NamingAvoid (avoid@explicit_intro_names l))
+      intro_forthcoming_then_gen (NamingAvoid (Id.Set.union avoid (explicit_intro_names l)))
 	  destopt onlydeps n bound
         (fun ids -> intro_patterns_core with_evars b avoid ids thin destopt bound
           (n+List.length ids) tac l)
@@ -2520,12 +2521,12 @@ and intro_pattern_naming loc with_evars b avoid ids pat thin destopt bound n tac
         intro_then_gen (NamingMustBe (loc,id)) destopt true false
           (fun id -> intro_patterns_core with_evars b avoid (id::ids) thin destopt bound n tac l))
   | IntroAnonymous ->
-      intro_then_gen (NamingAvoid (avoid@explicit_intro_names l))
+      intro_then_gen (NamingAvoid (Id.Set.union avoid (explicit_intro_names l)))
 	destopt true false
         (fun id -> intro_patterns_core with_evars b avoid (id::ids) thin destopt bound n tac l)
   | IntroFresh id ->
       (* todo: avoid thinned names to interfere with generation of fresh name *)
-      intro_then_gen (NamingBasedOn (id, avoid@explicit_intro_names l))
+      intro_then_gen (NamingBasedOn (id, Id.Set.union avoid (explicit_intro_names l)))
 	destopt true false
         (fun id -> intro_patterns_core with_evars b avoid (id::ids) thin destopt bound n tac l)
 
@@ -2559,7 +2560,7 @@ and prepare_intros ?loc with_evars dft destopt = function
   | IntroAction ipat ->
       prepare_naming ?loc dft,
       (let tac thin bound =
-        intro_patterns_core with_evars true [] [] thin destopt bound 0
+        intro_patterns_core with_evars true Id.Set.empty [] thin destopt bound 0
           (fun _ l -> clear_wildcards l) in
       fun id ->
         intro_pattern_action ?loc with_evars true true ipat [] destopt tac id)
@@ -2570,7 +2571,7 @@ let intro_patterns_head_core with_evars b destopt bound pat =
   Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
     check_name_unicity env [] [] pat;
-    intro_patterns_core with_evars b [] [] [] destopt
+    intro_patterns_core with_evars b Id.Set.empty [] [] destopt
       bound 0 (fun _ l -> clear_wildcards l) pat
   end
 
@@ -2682,8 +2683,8 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty =
     let (sigma, (newcl, eq_tac)) = match with_eq with
       | Some (lr,(loc,ido)) ->
           let heq = match ido with
-            | IntroAnonymous -> new_fresh_id [id] (add_prefix "Heq" id) gl
-            | IntroFresh heq_base -> new_fresh_id [id] heq_base gl
+            | IntroAnonymous -> new_fresh_id (Id.Set.singleton id) (add_prefix "Heq" id) gl
+            | IntroFresh heq_base -> new_fresh_id (Id.Set.singleton id) heq_base gl
             | IntroIdentifier id -> id in
           let eqdata = build_coq_eq_data () in
           let args = if lr then [t;mkVar id;c] else [t;c;mkVar id]in
@@ -2735,8 +2736,8 @@ let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty =
   match with_eq with
   | Some (lr,(loc,ido)) ->
       let heq = match ido with
-      | IntroAnonymous -> fresh_id_in_env [id] (add_prefix "Heq" id) env
-      | IntroFresh heq_base -> fresh_id_in_env [id] heq_base env
+      | IntroAnonymous -> fresh_id_in_env (Id.Set.singleton id) (add_prefix "Heq" id) env
+      | IntroFresh heq_base -> fresh_id_in_env (Id.Set.singleton id) heq_base env
       | IntroIdentifier id ->
           if List.mem id (ids_of_named_context (named_context env)) then
             user_err ?loc  (pr_id id ++ str" is already used.");
@@ -3143,13 +3144,13 @@ let rec consume_pattern avoid na isdep gl = function
   | (loc,IntroForthcoming true)::names when not isdep ->
       consume_pattern avoid na isdep gl names
   | (loc,IntroForthcoming _)::names as fullpat ->
-      let avoid = avoid@explicit_intro_names names in
+      let avoid = Id.Set.union avoid (explicit_intro_names names) in
       ((loc,intropattern_of_name gl avoid na), fullpat)
   | (loc,IntroNaming IntroAnonymous)::names ->
-      let avoid = avoid@explicit_intro_names names in
+      let avoid = Id.Set.union avoid (explicit_intro_names names) in
       ((loc,intropattern_of_name gl avoid na), names)
   | (loc,IntroNaming (IntroFresh id'))::names ->
-      let avoid = avoid@explicit_intro_names names in
+      let avoid = Id.Set.union avoid (explicit_intro_names names) in
       ((loc,IntroNaming (IntroIdentifier (new_fresh_id avoid id' gl))), names)
   | pat::names -> (pat,names)
 
@@ -3207,7 +3208,7 @@ let get_recarg_dest (recargdests,tophyp) =
 *)
 
 let induct_discharge with_evars dests avoid' tac (avoid,ra) names =
-  let avoid = avoid @ avoid' in
+  let avoid = Id.Set.union avoid avoid' in
   let rec peel_tac ra dests names thin =
     match ra with
     | (RecArg,_,deprec,recvarname) ::
@@ -3303,7 +3304,7 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac =
             (* Based on the knowledge given by the user, all
                constraints on the variable are generalizable in the
                current environment so that it is clearable after destruction *)
-	    atomize_one (i-1) (c::args) (c::args') (id::avoid)
+	    atomize_one (i-1) (c::args) (c::args') (Id.Set.add id avoid)
 	| _ ->
 	   let c' = expand_projections env' sigma c in
             let dependent t = dependent sigma c t in
@@ -3328,9 +3329,9 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac =
             let x = fresh_id_in_env avoid id env in
 	    Tacticals.New.tclTHEN
 	      (letin_tac None (Name x) c None allHypsAndConcl)
-	      (atomize_one (i-1) (mkVar x::args) (mkVar x::args') (x::avoid))
+	      (atomize_one (i-1) (mkVar x::args) (mkVar x::args') (Id.Set.add x avoid))
   in
-  atomize_one (List.length argl) [] [] []
+  atomize_one (List.length argl) [] [] Id.Set.empty
   end
 
 (* [cook_sign] builds the lists [beforetoclear] (preceding the
@@ -3402,7 +3403,7 @@ let cook_sign hyp0_opt inhyps indvars env sigma =
   (* First phase from L to R: get [toclear], [decldep] and [statuslist]
      for the hypotheses before (= more ancient than) hyp0 (see above) *)
   let toclear = ref [] in
-  let avoid = ref [] in
+  let avoid = ref Id.Set.empty in
   let decldeps = ref [] in
   let ldeps = ref [] in
   let rstatus = ref [] in
@@ -3419,7 +3420,7 @@ let cook_sign hyp0_opt inhyps indvars env sigma =
          is one of indvars too *)
       toclear := hyp::!toclear;
       MoveFirst (* fake value *)
-    end else if Id.List.mem hyp indvars then begin
+    end else if Id.Set.mem hyp indvars then begin
       (* The variables in indvars are such that they don't occur any
          more after generalization, so declare them to clear. *)
       toclear := hyp::!toclear;
@@ -3429,14 +3430,14 @@ let cook_sign hyp0_opt inhyps indvars env sigma =
 	(Option.cata (fun id -> occur_var_in_decl env sigma id decl) false hyp0_opt)
       in
       let depother = List.is_empty inhyps &&
-	(List.exists (fun id -> occur_var_in_decl env sigma id decl) indvars ||
+	(Id.Set.exists (fun id -> occur_var_in_decl env sigma id decl) indvars ||
          List.exists (fun decl' -> occur_var_in_decl env sigma (NamedDecl.get_id decl') decl) !decldeps)
       in
       if not (List.is_empty inhyps) && Id.List.mem hyp inhyps
          || dephyp0 || depother
       then begin
 	decldeps := decl::!decldeps;
-	avoid := hyp::!avoid;
+	avoid := Id.Set.add hyp !avoid;
         maindep := dephyp0 || !maindep;
 	if !before then begin
           toclear := hyp::!toclear;
@@ -3560,15 +3561,15 @@ let make_up_names n ind_opt cname =
     else add_prefix ind_prefix cname in
   let hyprecname = make_base n base_ind in
   let avoid =
-    if Int.equal n 1 (* Only one recursive argument *) || Int.equal n 0 then []
+    if Int.equal n 1 (* Only one recursive argument *) || Int.equal n 0 then Id.Set.empty
     else
       (* Forbid to use cname, cname0, hyprecname and hyprecname0 *)
       (* in order to get names such as f1, f2, ... *)
       let avoid =
-        (make_ident (Id.to_string hyprecname) None) ::
-        (make_ident (Id.to_string hyprecname) (Some 0)) :: [] in
+        Id.Set.add (make_ident (Id.to_string hyprecname) None)
+        (Id.Set.singleton (make_ident (Id.to_string hyprecname) (Some 0))) in
       if not (String.equal (atompart_of_id cname) "H") then
-        (make_ident base (Some 0)) :: (make_ident base None) :: avoid
+        Id.Set.add (make_ident base (Some 0)) (Id.Set.add (make_ident base None) avoid)
       else avoid in
   Id.of_string base, hyprecname, avoid
 
@@ -3727,10 +3728,10 @@ let abstract_args gl generalize_vars dep id defined f args =
   let env = Tacmach.New.pf_env gl in
   let concl = Tacmach.New.pf_concl gl in
   let dep = dep || local_occur_var !sigma id concl in
-  let avoid = ref [] in
+  let avoid = ref Id.Set.empty in
   let get_id name =
     let id = new_fresh_id !avoid (match name with Name n -> n | Anonymous -> Id.of_string "gen_x") gl in
-      avoid := id :: !avoid; id
+      avoid := Id.Set.add id !avoid; id
   in
     (* Build application generalized w.r.t. the argument plus the necessary eqs.
        From env |- c : forall G, T and args : G we build
@@ -4154,7 +4155,7 @@ let given_elim hyp0 (elimc,lbind as e) gl =
   Tacmach.New.project gl, (e, elimt), ind_type_guess
 
 type scheme_signature =
-    (Id.t list * (elim_arg_kind * bool * bool * Id.t) list) array
+    (Id.Set.t * (elim_arg_kind * bool * bool * Id.t) list) array
 
 type eliminator_source =
   | ElimUsing of (eliminator * EConstr.types) * scheme_signature
@@ -4345,7 +4346,7 @@ let induction_without_atomization isrec with_evars elim names lid =
        gt_wf_rec was taken as a functional scheme with no parameters,
        but by chance, because of the addition of at least hyp0 for
        cook_sign, it behaved as if there was a real induction arg. *)
-    if indvars = [] then [List.hd lid_params] else indvars in
+    if List.is_empty indvars then Id.Set.singleton (List.hd lid_params) else Id.Set.of_list indvars in
   let induct_tac elim = Tacticals.New.tclTHENLIST [
     (* pattern to make the predicate appear. *)
     reduce (Pattern (List.map inj_with_occurrences lidcstr)) onConcl;
@@ -4541,7 +4542,7 @@ let induction_gen clear_flag isrec with_evars elim
     let id =
     (* Type not the right one if partially applied but anyway for internal use*)
       let x = id_of_name_using_hdchar env evd t Anonymous in
-      new_fresh_id [] x gl in
+      new_fresh_id Id.Set.empty x gl in
     let info_arg = (is_arg_pure_hyp, not enough_applied) in
     pose_induction_arg_then
       isrec with_evars info_arg elim id arg t inhyps cls
@@ -4580,7 +4581,7 @@ let induction_gen_l isrec with_evars elim names lc =
                 let x =
 		  id_of_name_using_hdchar env sigma (type_of c) Anonymous in
 
-                let id = new_fresh_id [] x gl in
+                let id = new_fresh_id Id.Set.empty x gl in
 		let newl' = List.map (fun r -> replace_term sigma c (mkVar id) r) l' in
 		let _ = newlc:=id::!newlc in
 		Tacticals.New.tclTHEN
@@ -5017,7 +5018,7 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK =
         then (s1,push_named_context_val d s2)
 	else (Context.Named.add d s1,s2))
       global_sign (Context.Named.empty, empty_named_context_val) in
-  let id = next_global_ident_away id (pf_ids_of_hyps gl) in
+  let id = next_global_ident_away id (pf_ids_set_of_hyps gl) in
   let concl = match goal_type with
               | None ->  Proofview.Goal.concl gl
               | Some ty -> ty in
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index bca0c4c50..e07d514cd 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -49,18 +49,18 @@ val convert_leq     : constr -> constr -> unit Proofview.tactic
 
 (** {6 Introduction tactics. } *)
 
-val fresh_id_in_env : Id.t list -> Id.t -> env -> Id.t
-val fresh_id : Id.t list -> Id.t -> goal sigma -> Id.t
+val fresh_id_in_env : Id.Set.t -> Id.t -> env -> Id.t
+val fresh_id : Id.Set.t -> Id.t -> goal sigma -> Id.t
 val find_intro_names : rel_context -> goal sigma -> Id.t list
 
 val intro                : unit Proofview.tactic
 val introf               : unit Proofview.tactic
 val intro_move        : Id.t option -> Id.t move_location -> unit Proofview.tactic
-val intro_move_avoid  : Id.t option -> Id.t list -> Id.t move_location -> unit Proofview.tactic
+val intro_move_avoid  : Id.t option -> Id.Set.t -> Id.t move_location -> unit Proofview.tactic
 
   (** [intro_avoiding idl] acts as intro but prevents the new Id.t
      to belong to [idl] *)
-val intro_avoiding       : Id.t list -> unit Proofview.tactic
+val intro_avoiding       : Id.Set.t -> unit Proofview.tactic
 
 val intro_replacing      : Id.t -> unit Proofview.tactic
 val intro_using          : Id.t -> unit Proofview.tactic
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 59920742d..503508fc0 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -533,7 +533,7 @@ open Namegen
 let compute_bl_goal ind lnamesparrec nparrec =
   let eqI, eff = eqI ind lnamesparrec in
   let list_id = list_id lnamesparrec in
-  let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in
+  let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> Id.Set.add id l)) (List.map RelDecl.get_name lnamesparrec) Id.Set.empty in
   let create_input c =
     let x = next_ident_away (Id.of_string "x") avoid and
         y = next_ident_away (Id.of_string "y") avoid in
@@ -578,7 +578,7 @@ let compute_bl_tact mode bl_scheme_key ind lnamesparrec nparrec =
         ( List.map (fun (_,_,sbl,_ ) -> sbl) list_id )
       in
       let fresh_id s gl =
-          let fresh = fresh_id_in_env (!avoid) s (Proofview.Goal.env gl) in
+          let fresh = fresh_id_in_env (Id.Set.of_list !avoid) s (Proofview.Goal.env gl) in
           avoid := fresh::(!avoid); fresh
       in
       Proofview.Goal.enter begin fun gl ->
@@ -676,7 +676,7 @@ let _ = bl_scheme_kind_aux := fun () -> bl_scheme_kind
 let compute_lb_goal ind lnamesparrec nparrec =
   let list_id = list_id lnamesparrec in
   let eq = Lazy.force eq and tt = Lazy.force tt and bb = Lazy.force bb in
-  let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in
+  let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> Id.Set.add id l)) (List.map RelDecl.get_name lnamesparrec) Id.Set.empty in
   let eqI, eff = eqI ind lnamesparrec in
     let create_input c =
       let x = next_ident_away (Id.of_string "x") avoid and
@@ -722,7 +722,7 @@ let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec =
         ( List.map (fun (_,_,_,slb) -> slb) list_id )
       in
       let fresh_id s gl =
-          let fresh = fresh_id_in_env (!avoid) s (Proofview.Goal.env gl) in
+          let fresh = fresh_id_in_env (Id.Set.of_list !avoid) s (Proofview.Goal.env gl) in
           avoid := fresh::(!avoid); fresh
       in
       Proofview.Goal.enter begin fun gl ->
@@ -806,7 +806,7 @@ let compute_dec_goal ind lnamesparrec nparrec =
   check_not_is_defined ();
   let eq = Lazy.force eq and tt = Lazy.force tt and bb = Lazy.force bb in
   let list_id = list_id lnamesparrec in
-  let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in
+  let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> Id.Set.add id l)) (List.map RelDecl.get_name lnamesparrec) Id.Set.empty in
     let create_input c =
       let x = next_ident_away (Id.of_string "x") avoid and
           y = next_ident_away (Id.of_string "y") avoid in
@@ -870,7 +870,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
       ( List.map (fun (_,_,_,slb) -> slb) list_id )
   in
   let fresh_id s gl =
-      let fresh = fresh_id_in_env (!avoid) s (Proofview.Goal.env gl) in
+      let fresh = fresh_id_in_env (Id.Set.of_list !avoid) s (Proofview.Goal.env gl) in
       avoid := fresh::(!avoid); fresh
   in
   Proofview.Goal.enter begin fun gl ->
diff --git a/vernac/classes.ml b/vernac/classes.ml
index c21345a2a..0926c93e5 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -183,7 +183,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
 	    id
       | Anonymous ->
 	  let i = Nameops.add_suffix (id_of_class k) "_instance_0" in
-	    Namegen.next_global_ident_away i (Termops.ids_of_context env)
+	    Namegen.next_global_ident_away i (Termops.vars_of_env env)
   in
   let env' = push_rel_context ctx env in
   evars := Evarutil.nf_evar_map !evars;
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 4b36c2d07..2b97437e6 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -211,7 +211,8 @@ let compute_proof_name locality = function
         user_err ?loc  (pr_id id ++ str " already exists.");
       id
   | None ->
-      next_global_ident_away default_thm_id (Proof_global.get_all_proof_names ())
+    let avoid = Id.Set.of_list (Proof_global.get_all_proof_names ()) in
+      next_global_ident_away default_thm_id avoid
 
 let save_remaining_recthms (locality,p,kind) norm ctx binders body opaq i (id,(t_i,(_,imps))) =
   let t_i = norm t_i in
diff --git a/vernac/record.ml b/vernac/record.ml
index 4fb607dec..18e7796ca 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -457,7 +457,7 @@ let declare_class finite def cum poly ctx id idbuild paramimpls params arity
     let impls = implicits_of_context params in
       List.map (fun x -> impls @ Impargs.lift_implicits (succ len) x) fieldimpls
   in
-  let binder_name = Namegen.next_ident_away (snd id) (Termops.ids_of_context (Global.env())) in
+  let binder_name = Namegen.next_ident_away (snd id) (Termops.vars_of_env (Global.env())) in
   let impl, projs =
     match fields with
     | [LocalAssum (Name proj_name, field) | LocalDef (Name proj_name, _, field)] when def ->
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index ee84ff101..0c7599450 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -125,8 +125,8 @@ let make_cases_aux glob_ref =
 	       | [] -> []
 	       | (n,_)::l ->
 		   let n' = Namegen.next_name_away_with_default (Id.to_string Namegen.default_dependent_ident) n avoid in
-		   Id.to_string n' :: rename (n'::avoid) l in
-	     let al' = rename [] al in
+		   Id.to_string n' :: rename (Id.Set.add n' avoid) l in
+	     let al' = rename Id.Set.empty al in
 	     let consref = ConstructRef (ith_constructor_of_inductive ind (i + 1)) in
 	     (Libnames.string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty consref) :: al') :: l)
 	  tarr []
@@ -1230,7 +1230,7 @@ let vernac_reserve bl =
     let env = Global.env() in
     let sigma = Evd.from_env env in
     let t,ctx = Constrintern.interp_type env sigma c in
-    let t = Detyping.detype Detyping.Now false [] env (Evd.from_ctx ctx) (EConstr.of_constr t) in
+    let t = Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_ctx ctx) (EConstr.of_constr t) in
     let t,_ = Notation_ops.notation_constr_of_glob_constr (default_env ()) t in
     Reserve.declare_reserved_type idl t)
   in List.iter sb_decl bl