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

1 files changed, 3 insertions, 3 deletions

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