From d28304f6ba18ad9527a63cd01b39a5ad27526845 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 9 Sep 2017 21:47:17 +0200 Subject: 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). --- vernac/classes.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'vernac/classes.ml') 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; -- cgit v1.2.3