From 9672a8034d7bb8fb21c829e7819b995db43a612a Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Thu, 14 Dec 2017 15:32:46 +0100
Subject: [PATCH] Separate file updates.v

---
 _CoqProject                 |  1 +
 theories/base_logic/upred.v |  2 +-
 theories/bi/bi.v            |  2 +-
 theories/bi/interface.v     | 32 --------------------------------
 theories/bi/updates.v       | 33 +++++++++++++++++++++++++++++++++
 5 files changed, 36 insertions(+), 34 deletions(-)
 create mode 100644 theories/bi/updates.v

diff --git a/_CoqProject b/_CoqProject
index 1211cbed0..364dba269 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -29,6 +29,7 @@ theories/bi/interface.v
 theories/bi/derived_connectives.v
 theories/bi/derived_laws.v
 theories/bi/big_op.v
+theories/bi/updates.v
 theories/bi/bi.v
 theories/bi/tactics.v
 theories/bi/fractional.v
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index 4f016b1ec..e2246a5c3 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Export cmra updates.
-From iris.bi Require Export derived_connectives.
+From iris.bi Require Export derived_connectives updates.
 From stdpp Require Import finite.
 Set Default Proof Using "Type".
 Local Hint Extern 1 (_ ≼ _) => etrans; [eassumption|].
diff --git a/theories/bi/bi.v b/theories/bi/bi.v
index 8e90d845f..c0846ea37 100644
--- a/theories/bi/bi.v
+++ b/theories/bi/bi.v
@@ -1,4 +1,4 @@
-From iris.bi Require Export derived_laws big_op.
+From iris.bi Require Export derived_laws big_op updates.
 Set Default Proof Using "Type".
 
 Module Import bi.
diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index c14f5d56d..5636c7994 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -1,4 +1,3 @@
-From stdpp Require Import coPset.
 From iris.algebra Require Export ofe.
 Set Primitive Projections.
 
@@ -525,34 +524,3 @@ Proof. eapply sbi_mixin_later_false_em, sbi_sbi_mixin. Qed.
 End sbi_laws.
 
 End bi.
-
-Class BUpd (A : Type) : Type := bupd : A → A.
-Instance : Params (@bupd) 2.
-
-Notation "|==> Q" := (bupd Q)
-  (at level 99, Q at level 200, format "|==>  Q") : bi_scope.
-Notation "P ==∗ Q" := (P ⊢ |==> Q)
-  (at level 99, Q at level 200, only parsing) : stdpp_scope.
-Notation "P ==∗ Q" := (P -∗ |==> Q)%I
-  (at level 99, Q at level 200, format "P  ==∗  Q") : bi_scope.
-
-Class FUpd (A : Type) : Type := fupd : coPset → coPset → A → A.
-Instance: Params (@fupd) 4.
-
-Notation "|={ E1 , E2 }=> Q" := (fupd E1 E2 Q)
-  (at level 99, E1, E2 at level 50, Q at level 200,
-   format "|={ E1 , E2 }=>  Q") : bi_scope.
-Notation "P ={ E1 , E2 }=∗ Q" := (P -∗ |={E1,E2}=> Q)%I
-  (at level 99, E1,E2 at level 50, Q at level 200,
-   format "P  ={ E1 , E2 }=∗  Q") : bi_scope.
-Notation "P ={ E1 , E2 }=∗ Q" := (P -∗ |={E1,E2}=> Q)
-  (at level 99, E1, E2 at level 50, Q at level 200, only parsing) : stdpp_scope.
-
-Notation "|={ E }=> Q" := (fupd E E Q)
-  (at level 99, E at level 50, Q at level 200,
-   format "|={ E }=>  Q") : bi_scope.
-Notation "P ={ E }=∗ Q" := (P -∗ |={E}=> Q)%I
-  (at level 99, E at level 50, Q at level 200,
-   format "P  ={ E }=∗  Q") : bi_scope.
-Notation "P ={ E }=∗ Q" := (P -∗ |={E}=> Q)
-  (at level 99, E at level 50, Q at level 200, only parsing) : stdpp_scope.
diff --git a/theories/bi/updates.v b/theories/bi/updates.v
new file mode 100644
index 000000000..12a4558b0
--- /dev/null
+++ b/theories/bi/updates.v
@@ -0,0 +1,33 @@
+From stdpp Require Import coPset.
+From iris.bi Require Import interface.
+
+Class BUpd (A : Type) : Type := bupd : A → A.
+Instance : Params (@bupd) 2.
+
+Notation "|==> Q" := (bupd Q)
+  (at level 99, Q at level 200, format "|==>  Q") : bi_scope.
+Notation "P ==∗ Q" := (P ⊢ |==> Q)
+  (at level 99, Q at level 200, only parsing) : stdpp_scope.
+Notation "P ==∗ Q" := (P -∗ |==> Q)%I
+  (at level 99, Q at level 200, format "P  ==∗  Q") : bi_scope.
+
+Class FUpd (A : Type) : Type := fupd : coPset → coPset → A → A.
+Instance: Params (@fupd) 4.
+
+Notation "|={ E1 , E2 }=> Q" := (fupd E1 E2 Q)
+  (at level 99, E1, E2 at level 50, Q at level 200,
+   format "|={ E1 , E2 }=>  Q") : bi_scope.
+Notation "P ={ E1 , E2 }=∗ Q" := (P -∗ |={E1,E2}=> Q)%I
+  (at level 99, E1,E2 at level 50, Q at level 200,
+   format "P  ={ E1 , E2 }=∗  Q") : bi_scope.
+Notation "P ={ E1 , E2 }=∗ Q" := (P -∗ |={E1,E2}=> Q)
+  (at level 99, E1, E2 at level 50, Q at level 200, only parsing) : stdpp_scope.
+
+Notation "|={ E }=> Q" := (fupd E E Q)
+  (at level 99, E at level 50, Q at level 200,
+   format "|={ E }=>  Q") : bi_scope.
+Notation "P ={ E }=∗ Q" := (P -∗ |={E}=> Q)%I
+  (at level 99, E at level 50, Q at level 200,
+   format "P  ={ E }=∗  Q") : bi_scope.
+Notation "P ={ E }=∗ Q" := (P -∗ |={E}=> Q)
+  (at level 99, E at level 50, Q at level 200, only parsing) : stdpp_scope.
-- 
GitLab