diff --git a/opam b/opam
index fa500c0055e94958b489370ab267f86978f92da6..dfc47ab895b8eb775a3fbf6ca3b15a0ea1f4b7a7 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 6f25bc17c592c6cfbbbb9dd138989d28fc391a34..47d27a15e3ce714f5ea8fe97d6cd40797a3edc60 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 46f48b90e6f1c5289f4e475b146d0ed7256e04db..8883994c8711489d19d037db99aa0ac890134e23 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 03595309d8eb4cf3f0b0fef66d3457fb514f4444..7ef91fc46840adf62b653376dae14976054bdc78 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 f5a95cb55b5b70dc57e2a162f2a81bd9528545a8..57af8956dde3d30f213e1420774b51118de88eb4 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 3da2f344df209886afb0e601f75de3e79c1b4a2a..1af88df8a5395fb5cf2a3545b9ea64d9277b2a25 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 :=