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/cases.mli | |
| 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/cases.mli')
| -rw-r--r-- | pretyping/cases.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/pretyping/cases.mli b/pretyping/cases.mli index 428f64b99..7bdc604b8 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -49,16 +49,16 @@ val constr_of_pat : Evd.evar_map ref -> rel_context -> Glob_term.cases_pattern -> - Names.Id.t list -> + Names.Id.Set.t -> Glob_term.cases_pattern * (rel_context * constr * (types * constr list) * Glob_term.cases_pattern) * - Names.Id.t list + Names.Id.Set.t type 'a rhs = { rhs_env : env; - rhs_vars : Id.t list; - avoid_ids : Id.t list; + rhs_vars : Id.Set.t; + avoid_ids : Id.Set.t; it : 'a option} type 'a equation = |