From 53bad5194829adff7577f9598620d7ecf0c2e561 Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Fri, 4 Oct 2019 17:35:23 +0200
Subject: [PATCH] bump gpfsl

---
 opam                                | 2 +-
 theories/lang/arc.v                 | 8 ++++----
 theories/lang/lock.v                | 2 +-
 theories/lang/spawn.v               | 2 +-
 theories/logic/gps.v                | 4 ++--
 theories/typing/lib/rwlock/rwlock.v | 4 ++--
 6 files changed, 11 insertions(+), 11 deletions(-)

diff --git a/opam b/opam
index fa500c00..dfc47ab8 100644
--- a/opam
+++ b/opam
@@ -10,5 +10,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
 depends: [
-  "coq-gpfsl" { (= "dev.2019-09-20.0.0f49245e") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2019-10-04.0.7ef617f5") | (= "dev") }
 ]
diff --git a/theories/lang/arc.v b/theories/lang/arc.v
index 6f25bc17..47d27a15 100644
--- a/theories/lang/arc.v
+++ b/theories/lang/arc.v
@@ -146,7 +146,7 @@ Section ArcInv.
     (* I have seen all upgrades by strong that I'm involved in --- γs *)
     WkUps γsw q Ut ∗ SeenActs γs ls Ut)%I.
 
-  Definition weak_interp ls γi γs γsw : interpC Σ unitProtocol :=
+  Definition weak_interp ls γi γs γsw : interpO Σ unitProtocol :=
     (λ pb lw γw t _ v, ∃ st, ⌜v = #(Z_of_arcweak_st st)⌝ ∗
        if pb
        (* Full interp *)
@@ -190,7 +190,7 @@ Section ArcInv.
             end
     )%I.
 
-  Definition weak_noCAS γsw : interpCasC Σ unitProtocol :=
+  Definition weak_noCAS γsw : interpCasO Σ unitProtocol :=
     (λ _ _ t _ v, ⌜v = #(-1)⌝ ∗ ∃ t' : time, ⌜(t < t')%positive⌝ ∗ StrDownCert γsw t')%I.
 
   Definition StrResources lw ls t v γi γs γw γsw q Mt Dt :=
@@ -203,7 +203,7 @@ Section ArcInv.
     (* weak resources I need to keep to use weak *)
     StrWkTok γsw q)%I.
 
-  Definition strong_interp lw γi γw γsw: interpC Σ unitProtocol :=
+  Definition strong_interp lw γi γw γsw: interpO Σ unitProtocol :=
     (λ pb ls γs t _ v, ∃ st, ⌜v = #(Z_of_arcstrong_st st)⌝ ∗
       if pb
        (* Full interp *)
@@ -226,7 +226,7 @@ Section ArcInv.
             end
     )%I.
 
-  Definition strong_noCAS : interpCasC Σ unitProtocol :=
+  Definition strong_noCAS : interpCasO Σ unitProtocol :=
     (λ _ _ _ _ v, ⌜v = #0⌝)%I.
 
   Definition strong_arc t q l γi γs γw γsw : vProp :=
diff --git a/theories/lang/lock.v b/theories/lang/lock.v
index 46f48b90..8883994c 100644
--- a/theories/lang/lock.v
+++ b/theories/lang/lock.v
@@ -32,7 +32,7 @@ Section proof.
   Implicit Types (l : loc).
   Local Notation vProp := (vProp Σ).
 
-  Definition lock_interp (R : vProp) : interpC Σ unitProtocol :=
+  Definition lock_interp (R : vProp) : interpO Σ unitProtocol :=
     (λ pb _ _ _ _ v, ∃ b : bool, ⌜v = #b⌝ ∗
                  if pb then (if b then True else R) else True)%I.
 
diff --git a/theories/lang/spawn.v b/theories/lang/spawn.v
index 03595309..7ef91fc4 100644
--- a/theories/lang/spawn.v
+++ b/theories/lang/spawn.v
@@ -51,7 +51,7 @@ Definition finishEscrow γc γe γi c Ψ :=
                             ∃ v, (c >> 1) ↦ v ∗ Ψ v)])%I.
 
 (* GPS protocol interpretation *)
-Definition spawn_interp γe γi Ψ : interpC Σ unitProtocol :=
+Definition spawn_interp γe γi Ψ : interpO Σ unitProtocol :=
   (λ _ c γc _ _ v, ∃ b : bool, ⌜v = #b⌝ ∗
        if b then finishEscrow γc γe γi c Ψ else True)%I.
 
diff --git a/theories/logic/gps.v b/theories/logic/gps.v
index f5a95cb5..57af8956 100644
--- a/theories/logic/gps.v
+++ b/theories/logic/gps.v
@@ -7,7 +7,7 @@ Section gps_at_bor_SP.
 Context `{!noprolG Σ, !gpsG Σ Prtcl, !lftG view_Lat (↑histN) Σ} (N: namespace).
 Local Notation vProp := (vProp Σ).
 
-Implicit Types (IP : interpC Σ Prtcl) (IPC: interpCasC Σ Prtcl) (l : loc)
+Implicit Types (IP : interpO Σ Prtcl) (IPC: interpCasO Σ Prtcl) (l : loc)
                (s : pr_stateT Prtcl) (t : time) (v : val) (E : coPset) (q: Qp)
                (κ : lft) (γ : gname).
 
@@ -235,7 +235,7 @@ Context `{!noprolG Σ, !gpsG Σ Prtcl, !gpsExAgG Σ, !lftG view_Lat (↑histN) 
         (N: namespace).
 Local Notation vProp := (vProp Σ).
 
-Implicit Types (IP : interpC Σ Prtcl) (l : loc)
+Implicit Types (IP : interpO Σ Prtcl) (l : loc)
                (s : pr_stateT Prtcl) (t : time) (v : val) (E : coPset) (q: Qp)
                (κ : lft) (γ : gname).
 
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index 3da2f344..1af88df8 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -166,7 +166,7 @@ Section rwlock_inv.
   (* GPS protocol definitions *)
   Definition rwlock_interp
     (γs: gname) (α : lft) (tyO: vProp) (tyS: lft → vProp)
-    : interpC Σ unitProtocol :=
+    : interpO Σ unitProtocol :=
     (λ pb l γ t _ vs, ∃ st, ⌜vs = #(Z_of_rwlock_st st)⌝ ∗
        (□ (∀ κ q E, ⌜lftE ⊆ E⌝ -∗ &{κ}tyO -∗ q.[κ] ={E}=∗ (□ tyS κ) ∗ q.[κ])) ∗
        if pb
@@ -187,7 +187,7 @@ Section rwlock_inv.
             end
        else True)%I.
 
-  Definition rwlock_noCAS : interpCasC Σ unitProtocol :=
+  Definition rwlock_noCAS : interpCasO Σ unitProtocol :=
     (λ _ _ _ _ v, ⌜v = #(-1)⌝)%I.
 
   Definition rwlock_proto' l γ γs κ (tyO: vProp) (tyS: lft → vProp): vProp :=
-- 
GitLab