From e8fb0e28641c6c538dc001b3f922d2def766be2e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 28 Aug 2017 14:30:07 +0200
Subject: [PATCH] Small optimization for iSpecialize.
---
theories/proofmode/tactics.v | 9 ++++++++-
1 file changed, 8 insertions(+), 1 deletion(-)
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 890a1e6b0..965b59745 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -475,7 +475,14 @@ Tactic Notation "iSpecializeCore" open_constr(t) "as" constr(p) :=
let pat := spec_pat.parse pat in
lazymatch type of H with
| string =>
- lazymatch eval compute in (p && negb (existsb spec_pat_modal pat)) with
+ (* The lemma [tac_specialize_persistent_helper] allows one to use all
+ 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. *)
+ lazymatch eval compute in
+ (bool_decide (pat ≠[]) && p && negb (existsb spec_pat_modal pat)) with
| true =>
eapply tac_specialize_persistent_helper with _ H _ _ _;
[env_reflexivity || fail "iSpecialize:" H "not found"
--
GitLab