diff options
| author | Pierre-Marie Pédrot | 2017-09-09 21:47:17 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-09-28 16:51:21 +0200 |
| commit | d28304f6ba18ad9527a63cd01b39a5ad27526845 (patch) | |
| tree | ddd8c5d10f0d1e52c675e8e027053fac7f05f259 /proofs/clenv.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 'proofs/clenv.ml')
| -rw-r--r-- | proofs/clenv.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index ea60be31f0..5ef7fac814 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -557,7 +557,7 @@ let make_clenv_binding_gen hyps_only n env sigma (c,t) = function let clause = mk_clenv_from_env env sigma n (c,t) in clenv_constrain_dep_args hyps_only largs clause | ExplicitBindings lbind -> - let t = rename_bound_vars_as_displayed sigma [] [] t in + let t = rename_bound_vars_as_displayed sigma Id.Set.empty [] t in let clause = mk_clenv_from_env env sigma n (c, t) in clenv_match_args lbind clause @@ -605,7 +605,7 @@ let make_evar_clause env sigma ?len t = | Some n -> assert (0 <= n); n in (** FIXME: do the renaming online *) - let t = rename_bound_vars_as_displayed sigma [] [] t in + let t = rename_bound_vars_as_displayed sigma Id.Set.empty [] t in let rec clrec (sigma, holes) n t = if n = 0 then (sigma, holes, t) else match EConstr.kind sigma t with |