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).

7 files changed, 72 insertions, 71 deletions

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