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). --- plugins/firstorder/instances.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/firstorder') 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 *) -- cgit v1.2.3