From d28304f6ba18ad9527a63cd01b39a5ad27526845 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 9 Sep 2017 21:47:17 +0200 Subject: 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). --- plugins/omega/coq_omega.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'plugins/omega') diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 99493d698..ae1a563be 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -1760,7 +1760,7 @@ let onClearedName id tac = tclTHEN (tclTRY (clear [id])) (Proofview.Goal.nf_enter begin fun gl -> - let id = fresh_id [] id gl in + let id = fresh_id Id.Set.empty id gl in tclTHEN (introduction id) (tac id) end) @@ -1768,8 +1768,8 @@ let onClearedName2 id tac = tclTHEN (tclTRY (clear [id])) (Proofview.Goal.nf_enter begin fun gl -> - let id1 = fresh_id [] (add_suffix id "_left") gl in - let id2 = fresh_id [] (add_suffix id "_right") gl in + let id1 = fresh_id Id.Set.empty (add_suffix id "_left") gl in + let id2 = fresh_id Id.Set.empty (add_suffix id "_right") gl in tclTHENLIST [ introduction id1; introduction id2; tac id1 id2 ] end) -- cgit v1.2.3