From ac2fe511cb79ca769913f90249fa8e2563bf6dfe Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 9 Feb 2017 20:36:37 +0100
Subject: [PATCH] Fix `iDestruct foo as #pat` when `foo` contains a `>[...]`
spec pattern.
In this case, we cannot use all the hypotheses for proving the premises as well
as for the remaining goal.
---
theories/proofmode/spec_patterns.v | 3 +++
theories/proofmode/tactics.v | 9 +++++++--
2 files changed, 10 insertions(+), 2 deletions(-)
diff --git a/theories/proofmode/spec_patterns.v b/theories/proofmode/spec_patterns.v
index a33322ee4..a1633aa88 100644
--- a/theories/proofmode/spec_patterns.v
+++ b/theories/proofmode/spec_patterns.v
@@ -15,6 +15,9 @@ Inductive spec_pat :=
| SName : string → spec_pat
| SForall : spec_pat.
+Definition spec_pat_modal (p : spec_pat) : bool :=
+ match p with SGoal g => spec_goal_modal g | _ => false end.
+
Module spec_pat.
Inductive token :=
| TName : string → token
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 5c7637c9c..e622cb100 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -332,16 +332,21 @@ Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
persistent. If so, one can use all spatial hypotheses for both proving the
premises and the remaning goal. The argument [p] can either be a Boolean or an
introduction pattern, which will be coerced into [true] when it solely contains
-`#` or `%` patterns at the top-level. *)
+`#` or `%` patterns at the top-level.
+
+In case the specialization pattern in [t] states that the modality of the goal
+should be kept for one of the premises (i.e. [>[H1 .. Hn]] is used) then [p]
+defaults to [false] (i.e. spatial hypotheses are not preserved). *)
Tactic Notation "iSpecializeCore" open_constr(t) "as" constr(p) :=
let p := intro_pat_persistent p in
let t :=
match type of t with string => constr:(ITrm t hnil "") | _ => t end in
lazymatch t with
| ITrm ?H ?xs ?pat =>
+ let pat := spec_pat.parse pat in
lazymatch type of H with
| string =>
- lazymatch p with
+ lazymatch eval compute in (p && negb (existsb spec_pat_modal pat)) with
| true =>
eapply tac_specialize_persistent_helper with _ H _ _ _;
[env_cbv; reflexivity || fail "iSpecialize:" H "not found"
--
GitLab