Commit 202a6080 authored by Jonas Kastberg's avatar Jonas Kastberg

Deleted moved Iris specific stuff

parent a6825e8d
...@@ -67,15 +67,6 @@ Definition chanΣ : gFunctors := ...@@ -67,15 +67,6 @@ Definition chanΣ : gFunctors :=
Instance subG_chanΣ {Σ} : subG chanΣ Σ chanG Σ. Instance subG_chanΣ {Σ} : subG chanΣ Σ chanG Σ.
Proof. solve_inG. Qed. 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. Section channel.
Context `{!heapG Σ, !chanG Σ} (N : namespace). Context `{!heapG Σ, !chanG Σ} (N : namespace).
......
Markdown is supported
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