diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-09-09 21:47:17 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-09-28 16:51:21 +0200 |
| commit | d28304f6ba18ad9527a63cd01b39a5ad27526845 (patch) | |
| tree | ddd8c5d10f0d1e52c675e8e027053fac7f05f259 /vernac/lemmas.ml | |
| parent | b9740771e8113cb9e607793887be7a12587d0326 (diff) | |
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).
Diffstat (limited to 'vernac/lemmas.ml')
| -rw-r--r-- | vernac/lemmas.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 4b36c2d07..2b97437e6 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -211,7 +211,8 @@ let compute_proof_name locality = function user_err ?loc (pr_id id ++ str " already exists."); id | None -> - next_global_ident_away default_thm_id (Proof_global.get_all_proof_names ()) + let avoid = Id.Set.of_list (Proof_global.get_all_proof_names ()) in + next_global_ident_away default_thm_id avoid let save_remaining_recthms (locality,p,kind) norm ctx binders body opaq i (id,(t_i,(_,imps))) = let t_i = norm t_i in |