From 9bdef1bfb8c549bb62ef5669489f6d546b88f7ca Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 15 Dec 2018 12:31:09 +0100
Subject: [PATCH] Remove unused `tac_wand_intro_pure`.

---
 theories/proofmode/coq_tactics.v | 12 ------------
 1 file changed, 12 deletions(-)

diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 9d806d265..09cba8b02 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -210,18 +210,6 @@ Proof.
     by rewrite -{1}absorbingly_intuitionistically_into_persistently
       absorbingly_sep_l wand_elim_r HQ.
 Qed.
-Lemma tac_wand_intro_pure Δ P φ Q R :
-  FromWand R P Q →
-  IntoPure P φ →
-  TCOr (Affine P) (Absorbing Q) →
-  (φ → envs_entails Δ Q) → envs_entails Δ R.
-Proof.
-  rewrite /FromWand envs_entails_eq. intros <- ? HPQ HQ. apply wand_intro_l. destruct HPQ.
-  - rewrite -(affine_affinely P) (into_pure P) -persistent_and_affinely_sep_l.
-    by apply pure_elim_l.
-  - rewrite (into_pure P) -(persistent_absorbingly_affinely ⌜ _ ⌝%I) absorbingly_sep_lr.
-    rewrite -persistent_and_affinely_sep_l. apply pure_elim_l=> ?. by rewrite HQ.
-Qed.
 Lemma tac_wand_intro_drop Δ P Q R :
   FromWand R P Q →
   TCOr (Affine P) (Absorbing Q) →
-- 
GitLab