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/extratactics.ml4 | |
| 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/extratactics.ml4')
| -rw-r--r-- | plugins/ltac/extratactics.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index b4c6f9c90..a7aebf9e1 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -665,7 +665,7 @@ let hResolve id c occ t = let sigma = Proofview.Goal.sigma gl in let env = Termops.clear_named_body id (Proofview.Goal.env gl) in let concl = Proofview.Goal.concl gl in - let env_ids = Termops.ids_of_context env in + let env_ids = Termops.vars_of_env env in let c_raw = Detyping.detype Detyping.Now true env_ids env sigma c in let t_raw = Detyping.detype Detyping.Now true env_ids env sigma t in let rec resolve_hole t_hole = @@ -764,7 +764,7 @@ let case_eq_intros_rewrite x = mkCaseEq x; Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl gl in - let hyps = Tacmach.New.pf_ids_of_hyps gl in + let hyps = Tacmach.New.pf_ids_set_of_hyps gl in let n' = nb_prod (Tacmach.New.project gl) concl in let h = fresh_id_in_env hyps (Id.of_string "heq") (Proofview.Goal.env gl) in Tacticals.New.tclTHENLIST [ |