From 1a4f03482c7b79322dcdb227dfa814d02bd118ed Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 2 Nov 2017 00:27:16 +0100
Subject: [PATCH] Remove some wp lemmas that are not used for implementing
 tactics anymore.

---
 theories/heap_lang/lifting.v | 19 -------------------
 1 file changed, 19 deletions(-)

diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index b8d1570db..644becba6 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -184,23 +184,4 @@ Proof.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
   iModIntro. iSplit=>//. by iApply "HΦ".
 Qed.
-
-(** Proof rules for derived constructs *)
-Lemma wp_seq E e1 e2 Φ :
-  is_Some (to_val e1) → Closed [] e2 →
-  ▷ WP e2 @ E {{ Φ }} ⊢ WP Seq e1 e2 @ E {{ Φ }}.
-Proof. iIntros ([? ?] ?). rewrite -wp_pure_step_later; by eauto. Qed.
-
-Lemma wp_skip E Φ : ▷ Φ (LitV LitUnit) ⊢ WP Skip @ E {{ Φ }}.
-Proof. rewrite -wp_seq; last eauto. by rewrite -wp_value. Qed.
-
-Lemma wp_match_inl E e0 x1 e1 x2 e2 Φ :
-  is_Some (to_val e0) → Closed (x1 :b: []) e1 →
-  ▷ WP subst' x1 e0 e1 @ E {{ Φ }} ⊢ WP Match (InjL e0) x1 e1 x2 e2 @ E {{ Φ }}.
-Proof. iIntros ([? ?] ?) "?". rewrite -!wp_pure_step_later; by eauto. Qed.
-
-Lemma wp_match_inr E e0 x1 e1 x2 e2 Φ :
-  is_Some (to_val e0) → Closed (x2 :b: []) e2 →
-  ▷ WP subst' x2 e0 e2 @ E {{ Φ }} ⊢ WP Match (InjR e0) x1 e1 x2 e2 @ E {{ Φ }}.
-Proof. iIntros ([? ?] ?) "?". rewrite -!wp_pure_step_later; by eauto. Qed.
 End lifting.
-- 
GitLab