From 65bde879558aa728d7434f78eed9b196467d7ba8 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 26 Oct 2017 23:07:41 +0200
Subject: [PATCH] Removed a stray proof mode lemma.

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

diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 923cb4fd3..724e7175e 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -529,10 +529,6 @@ Proof.
   intros. rewrite envs_app_sound //; simpl.
   rewrite right_id. by apply wand_mono.
 Qed.
-Lemma tac_wand_intro_pure Î” P Ï† Q : IntoPure P Ï† â†’ (Ï† â†’ Î” âŠ¢ Q) â†’ Î” âŠ¢ P -âˆ— Q.
-Proof.
-  intros. by apply wand_intro_l; rewrite (into_pure P); apply pure_elim_sep_l.
-Qed.
 Lemma tac_wand_intro_drop Î” P Q : (Î” âŠ¢ Q) â†’ Î” âŠ¢ P -âˆ— Q.
 Proof. intros. apply wand_intro_l. by rewrite sep_elim_r. Qed.
 
-- 
GitLab