diff --git a/opam b/opam
index 330eb9dadadf360b36c1489be18864321db3a50b..e4fc5bc7b5afaa9418d5e4857f208500dc3c0e01 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-12-09.0.babe5bb8") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2019-12-10.0.c3e8211e") | (= "dev") }
 ]
diff --git a/theories/lang/arc.v b/theories/lang/arc.v
index 47d27a15e3ce714f5ea8fe97d6cd40797a3edc60..1696ed6e9be56a0a6b632e6400de61da1185a719 100644
--- a/theories/lang/arc.v
+++ b/theories/lang/arc.v
@@ -301,7 +301,8 @@ Section arc.
   Qed.
 
   Global Instance arc_inv_proper :
-    Proper (pointwise_relation _ (≡) ==> (≡) ==> eq ==> eq ==> eq ==> eq ==> eq ==> (≡))
+    Proper (pointwise_relation _ (≡) ==> (≡) ==>
+                eq ==> eq ==> eq ==> eq ==> eq ==> (≡))
            arc_inv.
   Proof.
     move => ?????????????????????. subst.
@@ -890,7 +891,7 @@ Section arc.
       (λ tr sr, strong_interp P1 (l >> 1) γi γw γsw true l γs tr sr #z).
     set R: time → unitProtocol → lit → vProp :=
       (λ _ _ _, StrongTok γsw q ∗ StrongMoveAuth γsw Mt ∗ StrMoves γsw q Mt)%I.
-    iMod (rel_True_intro True%I tid with "[//]") as "#rTrue".
+    iMod (rel_True_intro tid) as "#rTrue".
     (* here comes the CAS *)
     iApply (GPS_SWRaw_SharedWriter_CAS_int_strong (strong_interp P1 (l >> 1) γi γw γsw)
             _ strong_noCAS false Relaxed Relaxed Relaxed z #(z+1) _ _ _ (q/2) _
@@ -1107,7 +1108,7 @@ Section arc.
     set R: time → unitProtocol → lit → vProp :=
       (λ _ _ _, StrongDownAuth γsw DtA ∗ StrDowns γsw q Dt ∗
                 agown γsw (awk_n ((Some q, ε))))%I.
-    iMod (rel_True_intro True%I tid with "[//]") as "#rTrue".
+    iMod (rel_True_intro tid) as "#rTrue".
     (* here comes the CAS *)
     iApply (GPS_SWRaw_SharedWriter_CAS_int_weak (weak_interp P2 l γi γs γsw) _
             (weak_noCAS γsw) _ _ _ z #(z+1) _ _ _ _ True%I Q Q1 Q2 R _ Vb
@@ -1275,7 +1276,7 @@ Section arc.
       (λ tr sr, weak_interp P2 l γi γs γsw true (l >> 1) γw tr sr #z).
     set R: time → unitProtocol → lit → vProp :=
       (λ _ _ _, WeakTok γsw q ∗ StrongDownAuth γsw Dt)%I.
-    iMod (rel_True_intro True%I tid with "[//]") as "#rTrue".
+    iMod (rel_True_intro tid) as "#rTrue".
     (* here comes the CAS *)
     iApply (GPS_SWRaw_SharedWriter_CAS_int_strong (weak_interp P2 l γi γs γsw) _
             (weak_noCAS γsw) false Relaxed Relaxed Relaxed z #(z+1) _ _ _ _ _
@@ -1460,7 +1461,7 @@ Section arc.
       (λ tr sr, strong_interp P1 (l >> 1) γi γw γsw true l γs tr sr #z).
     set R: time → unitProtocol → lit → vProp :=
       (λ _ _ _, WeakUpAuth γsw UtA ∗ WkUps γsw q Ut)%I.
-    iMod (rel_True_intro True%I tid with "[//]") as "#rTrue".
+    iMod (rel_True_intro tid) as "#rTrue".
     (* here comes the CAS *)
     iApply (GPS_SWRaw_SharedWriter_CAS_int_weak (strong_interp P1 (l >> 1) γi γw γsw) _
             strong_noCAS Relaxed Relaxed Relaxed z #(z+1) _ _ _ _
@@ -2415,7 +2416,7 @@ Section arc.
     set R: time → unitProtocol → lit → vProp :=
       (λ _ _ _, StrongDownAuth γsw DtA ∗ StrDowns γsw q Dt ∗
                 agown γsw (awk_n ((Some q, ε))))%I.
-    iMod (rel_True_intro True%I tid with "[//]") as "#rTrue".
+    iMod (rel_True_intro tid) as "#rTrue".
     (* here comes the CAS *)
     iApply (GPS_SWRaw_SharedWriter_CAS_int_weak (weak_interp P2 l γi γs γsw) _
             (weak_noCAS γsw) _ _ _ 1 #(-1) _ _ _ _ True%I Q Q1 Q2 R _ Vb
@@ -2649,7 +2650,7 @@ Section arc.
       (λ tr sr, strong_interp P1 (l >> 1) γi γw γsw true l γs tr sr #1).
     set R: time → unitProtocol → lit → vProp :=
       (λ _ _ _, StrongTok γsw q ∗ StrongMoveAuth γsw Mt ∗ StrMoves γsw q Mt)%I.
-    iMod (rel_True_intro True%I tid with "[//]") as "#rTrue".
+    iMod (rel_True_intro tid) as "#rTrue".
     (* here comes the CAS *)
     iApply (GPS_SWRaw_SharedWriter_CAS_int_strong (strong_interp P1 (l >> 1) γi γw γsw) _
             strong_noCAS false _ _ _ 1 #0 _ _ _ q _
diff --git a/theories/lang/lock.v b/theories/lang/lock.v
index 8883994c8711489d19d037db99aa0ac890134e23..5c7ad23065f54ffb494d1ab6c3767dfa7e5d10c2 100644
--- a/theories/lang/lock.v
+++ b/theories/lang/lock.v
@@ -117,7 +117,7 @@ Section proof.
     iIntros "#LFT !#" (Φ) "[#Hproto Htok] HΦ". wp_rec.
     iDestruct "Hproto" as (R0) "[#Eq Hproto]".
     iDestruct "Hproto" as (t v) "PP".
-    iMod (rel_True_intro True%I tid with "[//]") as "#rTrue".
+    iMod (rel_True_intro tid) as "#rTrue".
     iApply (GPS_aPP_CAS_int_simple N (lock_interp R0) l κ q t () _
                 (Z_of_bool false) #true _ _ _ γ True%I (λ _ _, R0)%I
                 (λ t _, lock_interp R0 false l γ t () #false)
diff --git a/theories/logic/gps.v b/theories/logic/gps.v
index 6fb45cfdf85ac148913d604d3ad713c744d0c9d9..ce337cab525fc21505c9bc8bef68bac90ef0c57c 100644
--- a/theories/logic/gps.v
+++ b/theories/logic/gps.v
@@ -133,7 +133,7 @@ Lemma GPS_aSP_SharedWriter_CAS_int_weak
               (∀ t'' , ⌜(t' < t'')%positive⌝ -∗
                   ▷ GPS_SWSharedWriter l t'' s'' vw γ ={E ∖ ↑N}=∗
                   (<obj> (▷ Q1 t' s' ={E ∖ ↑N}=∗ ▷ IP false l γ t' s' #vr)) ∗
-                  |={E ∖ ↑N,E'}▷=> Q t'' s'' ∗ IP true l γ t'' s'' vw))) ) ∧
+                  |={E ∖ ↑N,E'}▷=> Q t'' s'' ∗ ▷ IP true l γ t'' s'' vw))) ) ∧
         ▷ (∀ (v: lit), ⌜lit_neq vr v⌝ -∗
         <obj> ((IP false l γ t' s' #v ={E ∖ ↑N}=∗ IP false l γ t' s' #v ∗ R t' s' v) ∧
                (IP true l γ t' s' #v ={E ∖ ↑N}=∗ IP true l γ t' s' #v ∗ R t' s' v) ∧
@@ -183,7 +183,7 @@ Lemma GPS_aSP_SharedWriter_CAS_int_strong
             (∀ t'' , ⌜(t' < t'')%positive⌝ -∗ ▷ GPS_SWSharedWriter l t'' s'' vw γ -∗
               (if dropR then ▷ GPS_SWSharedReader l t'' s'' vw qs γ else True) ={E ∖ ↑N}=∗
               (<obj> (▷ Q1 t' s' ={E ∖ ↑N}=∗ ▷ IP false l γ t' s' #vr)) ∗
-              |={E ∖ ↑N,E'}▷=> Q t'' s'' ∗ IP true l γ t'' s'' vw)) ) ∧
+              |={E ∖ ↑N,E'}▷=> Q t'' s'' ∗ ▷ IP true l γ t'' s'' vw)) ) ∧
       ▷ (∀ (v: lit), ⌜lit_neq vr v⌝ -∗
         <obj> ((IP false l γ t' s' #v ={E ∖ ↑N}=∗ IP false l γ t' s' #v ∗ R t' s' v) ∧
                (IP true l γ t' s' #v ={E ∖ ↑N}=∗ IP true l γ t' s' #v ∗ R t' s' v))))%I in
@@ -330,7 +330,7 @@ Lemma GPS_aPP_CAS_int_simple IP l κ q t s v (vr: Z) (vw: val) orf or ow γ
        (P -∗ ▷ Q2 t' s' ={E ∖ ↑N}=∗ ∃ s'', ⌜s' ⊑ s''⌝ ∗
           (∀ t , ⌜(t' < t)%positive⌝ -∗ ▷ (GPS_PP_Local l t s'' vw γ) ={E ∖ ↑N}=∗
               (<obj> (▷ Q1 t' s' ={E ∖ ↑N}=∗ ▷ IP false l γ t' s' #vr)) ∗
-              |={E ∖ ↑N}▷=> Q t s'' ∗ IP true l γ t s'' vw)) ) ∧
+              |={E ∖ ↑N}▷=> Q t s'' ∗ ▷ IP true l γ t s'' vw)) ) ∧
       (▷ ∀ (v: lit), ⌜lit_neq vr v⌝ -∗
           <obj> ((IP false l γ t' s' #v ={E ∖ ↑N}=∗
                     IP false l γ t' s' #v ∗ R t' s' v) ∧
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index 9c66a0550e0897e3ee4d10cffe8c95dbcc9349c3..a9367fe5c3647fe57e6fb5fdcbedcd871c9b6fa4 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -218,7 +218,7 @@ Section rwlock_functions.
         (λ t _, rwlock_interp γs β tyO tyS true lx γ t () #(Z_of_rwlock_st st'))%I.
       set R : time → () → lit → vProp Σ := (λ _ _ _, True)%I.
       set P : vProp Σ := (<obj> (qβ / 2).[β])%I.
-      iMod (rel_True_intro True%I tid with "[//]") as "#rTrue".
+      iMod (rel_True_intro tid) as "#rTrue".
 
       iApply (GPS_aSP_SharedWriter_CAS_int_weak rwlockN (rwlock_interp γs β tyO tyS)
                 rwlock_noCAS _ β _ _ _ _ (Z_of_rwlock_st st') #(Z_of_rwlock_st st' + 1)
@@ -279,7 +279,7 @@ Section rwlock_functions.
           + iExists (Some (inr (ν, (1 / 2)%Qp, 1%positive))). iSplitL ""; [done|].
             iFrame "Share g W'". iExists _. iFrame "H† Hshr Htok1 R2".
             rewrite Qp_div_2. iSplitR ""; [|done].
-            iIntros "Hν". iApply "Hh". rewrite -lft_dead_or. auto. }
+            iIntros "!> Hν". iApply "Hh". rewrite -lft_dead_or. auto. }
 
       iNext. simpl.
       iIntros (b t2 [] v2) "(Hβtok1&_& [([%[%%]]&_& Hβtok2 & Hβ) | ([% _] &_&_& P)])".
@@ -359,7 +359,7 @@ Section rwlock_functions.
         (λ t _, rwlock_interp γs β tyO tyS false lx γ t () #0)%I.
     set Q2: time → () → vProp Σ :=
         (λ t _, rwlock_interp γs β tyO tyS true lx γ t () #0)%I.
-    iMod (rel_True_intro True%I tid with "[//]") as "#rTrue".
+    iMod (rel_True_intro tid) as "#rTrue".
     iApply (GPS_aSP_SharedWriter_CAS_int_weak rwlockN
               (rwlock_interp γs β tyO tyS) rwlock_noCAS _ β qβ _ _ _
               0 #(-1) tP () _ _ True%I Q Q1 Q2 (λ _ _ _, True)%I _ (⊤ ∖ ↑rwlockN)