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). --- pretyping/unification.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping/unification.ml') 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" -- cgit v1.2.3