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 /proofs/tacmach.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 'proofs/tacmach.mli')
| -rw-r--r-- | proofs/tacmach.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 93bf428fd..7e6d83b10 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -48,7 +48,6 @@ val pf_get_hyp : goal sigma -> Id.t -> named_declaration val pf_get_hyp_typ : goal sigma -> Id.t -> types val pf_get_new_id : Id.t -> goal sigma -> Id.t -val pf_get_new_ids : Id.t list -> goal sigma -> Id.t list val pf_reduction_of_red_expr : goal sigma -> red_expr -> constr -> evar_map * constr @@ -120,6 +119,7 @@ module New : sig val pf_get_new_id : identifier -> 'a Proofview.Goal.t -> identifier val pf_ids_of_hyps : 'a Proofview.Goal.t -> identifier list + val pf_ids_set_of_hyps : 'a Proofview.Goal.t -> Id.Set.t val pf_hyps_types : 'a Proofview.Goal.t -> (identifier * types) list val pf_get_hyp : identifier -> 'a Proofview.Goal.t -> named_declaration |