From 2d3be60b01a14edc6a3ac4fdfcc683e0faffefed Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Thu, 22 Feb 2018 11:19:32 +0100
Subject: [PATCH] Bump Iris.

---
 opam                        | 2 +-
 theories/fractor.v          | 1 +
 theories/gps/fractional.v   | 2 +-
 theories/gps/plain.v        | 2 +-
 theories/gps/singlewriter.v | 2 +-
 theories/logically_atomic.v | 2 +-
 theories/rsl.v              | 4 ++--
 theories/wp_tactics.v       | 2 +-
 theories/wp_tactics_vProp.v | 2 +-
 9 files changed, 10 insertions(+), 9 deletions(-)

diff --git a/opam b/opam
index 6ec89d7e..b04df149 100644
--- a/opam
+++ b/opam
@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/igps" ]
 depends: [
-  "coq-iris" { (= "branch.gen_proofmode.2018-02-15.5") | (= "dev") }
+  "coq-iris" { (= "branch.gen_proofmode.2018-02-21.8") | (= "dev") }
 ]
diff --git a/theories/fractor.v b/theories/fractor.v
index 37b9d181..8edd8397 100644
--- a/theories/fractor.v
+++ b/theories/fractor.v
@@ -2,6 +2,7 @@ From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth frac excl gmap .
 From iris.bi Require Import big_op fractional.
 From iris.base_logic.lib Require Import cancelable_invariants.
+From stdpp Require Export namespaces.
 
 Import uPred.
 
diff --git a/theories/gps/fractional.v b/theories/gps/fractional.v
index ff160d85..a3ff8cd6 100644
--- a/theories/gps/fractional.v
+++ b/theories/gps/fractional.v
@@ -1,5 +1,5 @@
 From iris.proofmode Require Import tactics.
-From iris.base_logic Require Import iprop namespaces.
+From iris.base_logic Require Import iprop.
 From iris.program_logic Require Import ownp.
 From igps Require Import weakestpre. (* TODO: why ??? *)
 From igps.gps Require Export inst_shared.
diff --git a/theories/gps/plain.v b/theories/gps/plain.v
index 5fabc465..e1b73905 100644
--- a/theories/gps/plain.v
+++ b/theories/gps/plain.v
@@ -1,5 +1,5 @@
 From iris.proofmode Require Import tactics.
-From iris.base_logic Require Import iprop namespaces.
+From iris.base_logic Require Import iprop.
 From iris.program_logic Require Import ownp.
 From igps Require Import weakestpre. (* TODO: why ??? *)
 From igps.gps Require Export inst_shared.
diff --git a/theories/gps/singlewriter.v b/theories/gps/singlewriter.v
index 3ba264c4..4241635b 100644
--- a/theories/gps/singlewriter.v
+++ b/theories/gps/singlewriter.v
@@ -1,4 +1,4 @@
-From iris.base_logic Require Import iprop namespaces lib.cancelable_invariants.
+From iris.base_logic Require Import iprop lib.cancelable_invariants.
 From iris.proofmode Require Import tactics.
 From igps.gps Require Export inst_shared.
 From igps Require Import bigop.
diff --git a/theories/logically_atomic.v b/theories/logically_atomic.v
index d05b9532..7961c732 100644
--- a/theories/logically_atomic.v
+++ b/theories/logically_atomic.v
@@ -1,5 +1,5 @@
 From iris.proofmode Require Import tactics.
-From iris.base_logic Require Import iprop namespaces.
+From iris.base_logic Require Import iprop.
 From iris.program_logic Require Import ownp.
 From igps Require Import ghosts weakestpre invariants. (* TODO: why ??? *)
 Import base.
diff --git a/theories/rsl.v b/theories/rsl.v
index 89a49b8d..802845a5 100644
--- a/theories/rsl.v
+++ b/theories/rsl.v
@@ -934,8 +934,8 @@ Instance InitRaw_persistent V jγ : Persistent (InitRaw V jγ) := _.
       iSplitR ""; last iSplitL "".
       + rewrite /RSLInv /sts_inv.
         iExists j, γ. iModIntro. iSplitL ""; first by iNext.
-        iExists s'. iFrame "Own Hist' ress2".
-        iNext. iSplit; first auto. iNext. iSplitR "ressD"; last first.
+        iExists s'. rewrite /rsl_inv /s'. iFrame "Own Hist'". iSplit; first auto.
+        iSplitR "ressD ress2"; [|iSplitR "ress2"; [|done]]; last first; iNext; iNext.
         * iApply (big_sepS_subseteq _ _ h' with "[$ressD]").
           by rewrite H11 union_comm_L.
         * iApply (big_sepS_subseteq _ _ (gblock_ends l h') with "[$ress]").
diff --git a/theories/wp_tactics.v b/theories/wp_tactics.v
index 6f00bcf0..22e05c2f 100644
--- a/theories/wp_tactics.v
+++ b/theories/wp_tactics.v
@@ -8,7 +8,7 @@ Import uPred.
 Lemma tac_wp_pure `{ghosts.foundationG Σ} K Δ Δ' E e1 e2 φ Φ :
   PureExec (Λ:=ra_lang) φ e1 e2 →
   φ →
-  IntoLaterNEnvs 1 Δ Δ' →
+  MaybeIntoLaterNEnvs 1 Δ Δ' →
   envs_entails Δ' (WP fill K e2 @ E {{ Φ }}) →
   envs_entails Δ (WP fill K e1 @ E {{ Φ }}).
 Proof.
diff --git a/theories/wp_tactics_vProp.v b/theories/wp_tactics_vProp.v
index 9d2c5417..5d0640c7 100644
--- a/theories/wp_tactics_vProp.v
+++ b/theories/wp_tactics_vProp.v
@@ -19,7 +19,7 @@ Ltac wp_expr_simpl_subst := wp_expr_eval simpl_subst.
 Lemma tac_wp_pure `{foundationG Σ} Δ Δ' E e1 e2 φ Φ :
   (PureExec (Λ:=surface_lang) φ (e1) (e2)) →
   φ →
-  IntoLaterNEnvs 1 Δ Δ' →
+  MaybeIntoLaterNEnvs 1 Δ Δ' →
   envs_entails Δ' (WP e2 @ E {{ Φ }}) →
   envs_entails Δ (WP e1 @ E {{ Φ }}).
 Proof.
-- 
GitLab