From a3a5c714054f1e1b55438975332a37f5647f23db Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Fri, 2 Mar 2018 16:11:28 +0100
Subject: [PATCH] Bump Iris.

---
 opam                          |  2 +-
 theories/examples/spin_lock.v |  3 ++-
 theories/gps/plain.v          |  9 +++++----
 theories/gps/singlewriter.v   | 10 ++++++----
 theories/na.v                 |  4 ++--
 theories/proofmode.v          |  9 +++++----
 theories/weakestpre.v         |  7 +++++--
 7 files changed, 26 insertions(+), 18 deletions(-)

diff --git a/opam b/opam
index 21900742..8565a7ba 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-03-1.3") | (= "dev") }
+  "coq-iris" { (= "branch.gen_proofmode.2018-03-02.0") | (= "dev") }
 ]
diff --git a/theories/examples/spin_lock.v b/theories/examples/spin_lock.v
index 9370a21d..f7cf459d 100644
--- a/theories/examples/spin_lock.v
+++ b/theories/examples/spin_lock.v
@@ -32,7 +32,8 @@ Section proof.
   Local Open Scope VP.
   Notation Q_dup := (λ v, (v = 1) ∨ (v = 0)).
   Notation Q J := (λ v, (v = 1) ∨ (v = 0 ∧ J)).
-  Instance Frame_Into_Q (J : vPred) v : ∀ V, Frame false (J V) (Q J v V) (Q_dup v V)%V.
+  Instance Frame_Into_Q (J : vPred) v :
+    ∀ V, KnownFrame false (J V) (Q J v V) (Q_dup v V)%V.
   Proof. iIntros (V) "[oJ [%|%]]"; [by iLeft|iRight]. by iFrame "oJ". Qed.
 
   Definition isLock (l : loc) J : vPred :=
diff --git a/theories/gps/plain.v b/theories/gps/plain.v
index e1b73905..b681c07f 100644
--- a/theories/gps/plain.v
+++ b/theories/gps/plain.v
@@ -61,11 +61,12 @@ Section Plain.
     apply persistor_persistent => ?. apply _.
   Qed.
 
-  Local Instance : Frame false (gps_inv IP l γ γ_x) (gpsPRaw p l (encode (p,γ,γ_x,γx)))
-                         (Writer γ ζ ∗ exwr γ_x 1%Qp e_x ∗ own.own γx (DecAgree e_x)).
+  Local Instance :
+    KnownFrame false (gps_inv IP l γ γ_x) (gpsPRaw p l (encode (p,γ,γ_x,γx)))
+               (Writer γ ζ ∗ exwr γ_x 1%Qp e_x ∗ own.own γx (DecAgree e_x)).
   Proof.
-    intros. rewrite /Frame. iIntros "[? ?]". iExists _, _. iFrame "∗". iExists _, _, _.
-    cbn. by iFrame "∗".
+    intros. rewrite /KnownFrame /Frame. iIntros "[? ?]". iExists _, _.
+    iFrame "∗". iExists _, _, _. cbn. by iFrame "∗".
   Qed.
 
   Lemma GPS_PPs_agree l p s1 s2 (E : coPset) (HE: ↑persist_locN .@ l ⊆ E):
diff --git a/theories/gps/singlewriter.v b/theories/gps/singlewriter.v
index 4241635b..2eb60a74 100644
--- a/theories/gps/singlewriter.v
+++ b/theories/gps/singlewriter.v
@@ -72,9 +72,11 @@ Section Gname_StrongSW.
   Close Scope I.
 
   Local Instance :
-    Frame false (gps_inv (IP γ) l γ γ_x)
+    KnownFrame false (gps_inv (IP γ) l γ γ_x)
           (gpsSWnRaw γ l (encode (γ, (γ_x)))) True.
-  Proof. intros. rewrite /Frame /=. iIntros "[? _]". iExists _. by iFrame "∗". Qed.
+  Proof.
+    intros. rewrite /KnownFrame /Frame /=. iIntros "[? _]". iExists _. by iFrame "∗".
+  Qed.
 
   Lemma GPS_nFWP_Init_strong l (s: gname -> pr_state Prtcl) v
     (Q : gname -> vPred) (E : coPset) (HEN : ↑physN ⊆ E):
@@ -1022,9 +1024,9 @@ Section SingleWriter.
   Definition vGPS_FWP_eq : vGPS_FWP = _ := seal_eq _.
 
   Local Instance :
-    Frame false (gps_inv IP l γ γ_x) (gpsSWRaw l (encode (γ, (γ_x)))) True.
+    KnownFrame false (gps_inv IP l γ γ_x) (gpsSWRaw l (encode (γ, (γ_x)))) True.
   Proof.
-    intros. unfold Frame, bi_affinely_if, bi_persistently_if.
+    intros. unfold KnownFrame, Frame, bi_affinely_if, bi_persistently_if.
     iIntros "[H _]". iExists _, _. by iFrame "∗".
   Qed.
   Local Close Scope I.
diff --git a/theories/na.v b/theories/na.v
index b682fc40..1e6138ed 100644
--- a/theories/na.v
+++ b/theories/na.v
@@ -57,9 +57,9 @@ Section Exclusive.
   (* Proof. apply _. Qed. *)
 
   Global Instance Frame_na_ownloc l v:
-    Frame false ((own_loc_na l v)) (own_loc l) (True%I) | 1.
+    KnownFrame false ((own_loc_na l v)) (own_loc l) (True%I) | 1.
   Proof.
-    rewrite /own_loc_na /own_loc /Frame. iStartProof (uPred _).
+    rewrite /own_loc_na /own_loc /KnownFrame /Frame. iStartProof (uPred _).
     iIntros (?) "[H _] /=". iDestruct "H" as (?) "?". iExists _. eauto.
   Qed.
 
diff --git a/theories/proofmode.v b/theories/proofmode.v
index fe8ea4f1..d1ec1415 100644
--- a/theories/proofmode.v
+++ b/theories/proofmode.v
@@ -2,10 +2,11 @@ From iris.proofmode Require Export tactics.
 From igps Require Import viewpred.
 
 Global Instance Frame_vPred Σ p (P : vProp Σ) :
-  (* Frame (P V') (Q V') R → *)
-  (* class_instances.MakeSep ⌜V ⊑ V'⌝ R T → *)
-  Frame p (monPred_at P V) (monPred_at P V') ⌜V ⊑ V'⌝ | 30.
-Proof. intros. unfold Frame. iIntros "[? %]". rewrite H. by destruct p => /=. Qed.
+  KnownFrame p (monPred_at P V) (monPred_at P V') ⌜V ⊑ V'⌝ | 30.
+Proof.
+  intros. unfold KnownFrame, Frame. iIntros "[? %]".
+  rewrite H. by destruct p => /=.
+Qed.
 Hint Extern 10 (IsBiIndexRel _ _) => unfold IsBiIndexRel; solve_jsl
             : typeclass_instances.
 
diff --git a/theories/weakestpre.v b/theories/weakestpre.v
index 6d3e29cb..8ff3ed15 100644
--- a/theories/weakestpre.v
+++ b/theories/weakestpre.v
@@ -359,8 +359,11 @@ Section proofmode_classes.
   Qed.
 
   Global Instance frame_wp p E e R Φ Ψ :
-    (∀ v, Frame p R (Φ v) (Ψ v)) → Frame p R (WP e @ E {{ Φ }}) (WP e @ E {{ Ψ }}).
-  Proof. rewrite /Frame=> HR. rewrite wp_frame_l. apply wp_mono, HR. Qed.
+    (∀ v, Frame p R (Φ v) (Ψ v)) →
+    KnownFrame p R (WP e @ E {{ Φ }}) (WP e @ E {{ Ψ }}).
+  Proof.
+    rewrite /KnownFrame /Frame=> HR. rewrite wp_frame_l. apply wp_mono, HR.
+  Qed.
 
   Global Instance is_except_0_wp E e Φ : IsExcept0 (WP e @ E {{ Φ }}).
   Proof. by rewrite /IsExcept0 -{2}fupd_wp -except_0_fupd -fupd_intro. Qed.
-- 
GitLab