From 202a6080e169bcc6ee568c4193081ca42c22ea72 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Mon, 14 Oct 2019 13:42:33 -0400
Subject: [PATCH] Deleted moved Iris specific stuff

---
 theories/channel/channel.v | 9 ---------
 1 file changed, 9 deletions(-)

diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index 2a396eb..f7bf1dc 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -67,15 +67,6 @@ Definition chanΣ : gFunctors :=
 Instance subG_chanΣ {Σ} : subG chanΣ Σ → chanG Σ.
 Proof. solve_inG. Qed.
 
-(** MOVE TO IRIS *)
-Global Instance fst_atomic a v1 v2 : Atomic a (Fst (v1,v2)%V).
-Proof.
-  apply strongly_atomic_atomic, ectx_language_atomic;
-    [inversion 1; naive_solver
-    |apply ectxi_language_sub_redexes_are_values; intros [] **; naive_solver].
-Qed.
-
-
 Section channel.
   Context `{!heapG Σ, !chanG Σ} (N : namespace).
 
-- 
GitLab