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 /interp/impargs.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 'interp/impargs.ml')
| -rw-r--r-- | interp/impargs.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/impargs.ml b/interp/impargs.ml index d8241c044..09a0ba83c 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -255,7 +255,7 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t = in match kind_of_term (whd_all env t) with | Prod (na,a,b) -> - let na',avoid = find_displayed_name_in all [] na ([],b) in + let na',avoid = find_displayed_name_in all Id.Set.empty na ([],b) in let v = aux (push_rel (LocalAssum (na',a)) env) avoid 1 [na'] b in !rigid, Array.to_list v | _ -> true, [] |