From d2b71e0ab4bcb409f2f46c494e7b18f5ab0ba818 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers
Date: Tue, 1 Nov 2016 10:05:14 +0100
Subject: [PATCH] Instantiate foralls behind boxes by removing those.
That's like what we are doing when instantiating an arrow or wand.
---
proofmode/coq_tactics.v | 3 +++
1 file changed, 3 insertions(+)
diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v
index 314356e6..39abdb11 100644
--- a/proofmode/coq_tactics.v
+++ b/proofmode/coq_tactics.v
@@ -787,6 +787,9 @@ Global Instance forall_specialize_cons A As x xs Φ (Ψ : A → himpl As (uPred
(∀ x, ForallSpecialize xs (Φ x) (Ψ x)) →
ForallSpecialize (hcons x xs) (∀ x : A, Φ x) Ψ.
Proof. rewrite /ForallSpecialize /= => <-. by rewrite (forall_elim x). Qed.
+Global Instance forall_specialize_always As xs P (Ψ : himpl As (uPred M)) :
+ ForallSpecialize xs P Ψ → ForallSpecialize xs (□ P) Ψ | 101.
+Proof. rewrite /ForallSpecialize=> ->. by rewrite always_elim. Qed.
Lemma tac_forall_specialize {As} Δ Δ' i p P (Φ : himpl As (uPred M)) Q xs :
envs_lookup i Δ = Some (p, P) → ForallSpecialize xs P Φ →
--
GitLab