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 /pretyping/constr_matching.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 'pretyping/constr_matching.ml')
| -rw-r--r-- | pretyping/constr_matching.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index ca7f633dc..0973d73ee 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -178,7 +178,7 @@ let push_binder na1 na2 t ctx = let id2 = match na2 with | Name id2 -> id2 | Anonymous -> - let avoid = List.map pi2 ctx in + let avoid = Id.Set.of_list (List.map pi2 ctx) in Namegen.next_ident_away Namegen.default_non_dependent_ident avoid in (na1, id2, t) :: ctx |