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 /plugins/funind/functional_principles_proofs.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 'plugins/funind/functional_principles_proofs.ml')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 5f6d783598..bd5fb1d923 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -587,7 +587,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos = tclTHENLIST [ (* We first introduce the variables *) - tclDO nb_first_intro (Proofview.V82.of_tactic (intro_avoiding dyn_infos.rec_hyps)); + tclDO nb_first_intro (Proofview.V82.of_tactic (intro_avoiding (Id.Set.of_list dyn_infos.rec_hyps))); (* Then the equation itself *) Proofview.V82.of_tactic (intro_using heq_id); onLastHypId (fun heq_id -> tclTHENLIST [ @@ -1614,7 +1614,7 @@ let prove_principle_for_gen let hid = next_ident_away_in_goal (Id.of_string "prov") - hyps + (Id.Set.of_list hyps) in tclTHENLIST [ |