Skip to content
Snippets Groups Projects
Commit 65bde879 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Removed a stray proof mode lemma.

parent fe17c6af
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/proofmode/coq_tactics.v
+ 0
− 4
View file @ 65bde879
...@@ -529,10 +529,6 @@ Proof. ...@@ -529,10 +529,6 @@ Proof.
intros. rewrite envs_app_sound //; simpl. intros. rewrite envs_app_sound //; simpl.
rewrite right_id. by apply wand_mono. rewrite right_id. by apply wand_mono.
Qed. 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. Lemma tac_wand_intro_drop Δ P Q : (Δ ⊢ Q) → Δ ⊢ P -∗ Q.
Proof. intros. apply wand_intro_l. by rewrite sep_elim_r. Qed. Proof. intros. apply wand_intro_l. by rewrite sep_elim_r. Qed.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment