From a94cfec903b0df0368e6122b951fb385ff744520 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 5 Aug 2016 13:27:13 +0200
Subject: [PATCH] Add missing file program_logic/iris.

---
 program_logic/iris.v | 29 +++++++++++++++++++++++++++++
 1 file changed, 29 insertions(+)
 create mode 100644 program_logic/iris.v

diff --git a/program_logic/iris.v b/program_logic/iris.v
new file mode 100644
index 000000000..9165cbca0
--- /dev/null
+++ b/program_logic/iris.v
@@ -0,0 +1,29 @@
+From iris.program_logic Require Export ghost_ownership language.
+From iris.prelude Require Export coPset.
+From iris.algebra Require Import gmap auth agree gset coPset upred_big_op.
+
+Class irisPreG (Λ : language) (Σ : gFunctors) : Set := IrisPreG {
+  state_inG :> inG Σ (authUR (optionUR (exclR (stateC Λ))));
+  invariant_inG :> inG Σ (authUR (gmapUR positive (agreeR (laterC (iPreProp Σ)))));
+  enabled_inG :> inG Σ coPset_disjUR;
+  disabled_inG :> inG Σ (gset_disjUR positive);
+}.
+
+Class irisG (Λ : language) (Σ : gFunctors) : Set := IrisG {
+  iris_pre_inG :> irisPreG Λ Σ;
+  state_name : gname;
+  invariant_name : gname;
+  enabled_name : gname;
+  disabled_name : gname;
+}.
+
+Definition irisPreGF (Λ : language) : gFunctorList :=
+  [GFunctor (constRF (authUR (optionUR (exclR (stateC Λ)))));
+   GFunctor (authRF (gmapURF positive (agreeRF (laterCF idCF))));
+   GFunctor (constRF coPset_disjUR);
+   GFunctor (constRF (gset_disjUR positive))].
+
+Instance inGF_barrierG `{H : inGFs Σ (irisPreGF Λ)} : irisPreG Λ Σ.
+Proof.
+  by destruct H as (?%inGF_inG & ?%inGF_inG & ?%inGF_inG & ?%inGF_inG & _).
+Qed.
-- 
GitLab