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 /plugins/ltac/rewrite.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 'plugins/ltac/rewrite.mli')
-rw-r--r-- | plugins/ltac/rewrite.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli index 23767c12f..63e891b45 100644 --- a/plugins/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli @@ -110,7 +110,7 @@ val setoid_transitivity : constr option -> unit Proofview.tactic val apply_strategy : strategy -> Environ.env -> - Names.Id.t list -> + Names.Id.Set.t -> constr -> bool * constr -> evars -> rewrite_result |