From 726366bb2fb725c801b074565285facced9f0bef Mon Sep 17 00:00:00 2001
From: David Swasey <swasey@mpi-sws.org>
Date: Sat, 17 Dec 2016 15:48:20 +0100
Subject: [PATCH] Revert git:00444b0 as the weaker notion of atomicity is too
 weak for unsafe WP.

---
 theories/program_logic/language.v | 2 --
 1 file changed, 2 deletions(-)

diff --git a/theories/program_logic/language.v b/theories/program_logic/language.v
index 8189151d5..d600c5e75 100644
--- a/theories/program_logic/language.v
+++ b/theories/program_logic/language.v
@@ -82,8 +82,6 @@ Section language.
   Proof. unfold reducible, irreducible. naive_solver. Qed.
   Lemma reducible_not_val e σ : reducible e σ → to_val e = None.
   Proof. intros (?&?&?&?); eauto using val_stuck. Qed.
-  Lemma val_irreducible e σ : is_Some (to_val e) → irreducible e σ.
-  Proof. intros [??] ??? ?%val_stuck. by destruct (to_val e). Qed.
   Global Instance of_val_inj : Inj (=) (=) (@of_val Λ).
   Proof. by intros v v' Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
 
-- 
GitLab