From 51d94abb1d42e0ebd8b3602a0df227db1f1b084e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 31 Jul 2018 21:57:52 +0200
Subject: [PATCH] Clarify comment.
---
theories/proofmode/ltac_tactics.v | 5 +++--
1 file changed, 3 insertions(+), 2 deletions(-)
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 14169ca49..581c3b63e 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -667,8 +667,9 @@ Tactic Notation "iSpecializeCore" open_constr(H)
spatial hypotheses for both proving the premises of the lemma we
specialize as well as those of the remaining goal. We can only use it when
the result of the specialization is persistent, and no modality is
- eliminated. As an optimization, we do not use this when only universal
- quantifiers are instantiated. *)
+ eliminated. We do not use [tac_specialize_persistent_helper] in the case
+ only universal quantifiers and no implications or wands are instantiated
+ (i.e [pat = []]) because it is a.) not needed, and b.) more efficient. *)
let pat := spec_pat.parse pat in
lazymatch eval compute in
(p && bool_decide (pat ≠[]) && negb (existsb spec_pat_modal pat)) with
--
GitLab