diff --git a/opam b/opam
index f83032d285fae24d1e9c7740abdc984a326976fd..fa500c0055e94958b489370ab267f86978f92da6 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-19.0.5c030976") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2019-09-20.0.0f49245e") | (= "dev") }
 ]
diff --git a/theories/lang/arc.v b/theories/lang/arc.v
index fbb6da04a08de8b308bfd13dde4970c31660a534..6f25bc17c592c6cfbbbb9dd138989d28fc391a34 100644
--- a/theories/lang/arc.v
+++ b/theories/lang/arc.v
@@ -1,11 +1,11 @@
 From Coq.QArith Require Import Qcanon.
-From iris.base_logic.lib Require Import invariants.
-From iris.proofmode Require Import tactics.
 From iris.bi Require Import fractional.
+From iris.proofmode Require Import tactics.
 From iris.algebra Require Import excl csum frac auth agree.
-From lrust.lang Require Import notation new_delete arc_cmra.
-From gpfsl.logic Require Import view_invariants.
+From iris.base_logic.lib Require Import invariants.
 From gpfsl.gps Require Import middleware protocols.
+From gpfsl.logic Require Import view_invariants.
+From lrust.lang Require Import notation new_delete arc_cmra.
 Set Default Proof Using "Type".
 
 (* Rust Arc has a maximum number of clones to prevent overflow. We currently
@@ -728,13 +728,13 @@ Section arc.
     { iIntros "!>" (t' [] v' [_ Ext']). rewrite /StrongTok. iIntros "!>". iSplit.
       - iIntros "#SI !>". iFrame "SI SMA". rewrite /StrongTok. iFrame "St".
         iDestruct "SI" as (st) "[% Eq]". subst v'. iExists (Z_of_arcstrong_st st).
-        destruct st as [[]|]; simpl; [|done]. iPureIntro. split; [done|lia].
+        destruct st as [[]|]; simpl; [|done]. iPureIntro. split; [done|split].
       - iDestruct 1 as (st) "(Eq1 & SA & SI)". iDestruct "Eq1" as %?. subst v'.
         destruct st as [[q' n]|]; simpl.
         + iModIntro. iFrame "SMA". rewrite /StrongTok. iFrame "St".
           iSplitR""; [iExists (Some (q',n))|iExists (Z.pos n)].
           * iSplitL""; [done|]. by iFrame.
-          * iPureIntro. split; [done|lia].
+          * iPureIntro. split; [done|split].
         + iDestruct (StrongTok_Auth_agree with "[$SA St]") as %(?&?&EQ&?).
           rewrite /StrongTok. iFrame "St". done. }
     iIntros "!>" (t' [] v'). iDestruct 1 as "(_ & RR' & IS & Rs & St & SMA)".
@@ -1723,7 +1723,7 @@ Section arc.
           iSplitR "SD"; [iExists _; iFrame "WU SeenU'"|]. by iExists _.
         + iSplitL "SDA". { rewrite /Q Pos2Z.id decide_False; [|done].
                            iSplitR ""; [by iExists _|done]. }
-          rewrite decide_False; last first. { destruct n; try lia. done. }
+          rewrite decide_False; last first. { by destruct n; try lia. }
           iDestruct "WA" as (q2 Eq2) "WA".
           iExists (None, Some $ Cinl (q2, Pos.pred n)). iSplitL "".
           { iPureIntro. f_equal. by rewrite Z.sub_1_r -Pos2Z.inj_pred. }
@@ -2174,7 +2174,7 @@ Section arc.
         { by rewrite Qp_plus_assoc (Qp_plus_comm q2). } iFrame "HP".
         iExists _,_. iFrame "R' SM SD SeenD' oW".
         rewrite /Mt' (decide_False _ _ nEq). iFrame "SeenM'".
-        rewrite decide_False; last first. { simpl. destruct n; try lia. done. }
+        rewrite decide_False; last first. { simpl. by destruct n; try lia. }
         rewrite -Qp_plus_div. by iFrame "tok tok'". }
 
     (* finally done with the CAS *)
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index 967f2d59352ae43cab311b9720247eabe20ebb33..6b25d86c69c92231d6e014754e28b81b013a7d3c 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -1,16 +1,16 @@
 From Coq.QArith Require Import Qcanon.
 
+From iris.bi Require Import fractional.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth csum frac agree.
-From iris.bi Require Import fractional.
+
+From gpfsl.gps Require Import middleware protocols escrows.
 
 From lrust.lang Require Import memcpy arc arc_cmra.
 From lrust.lifetime Require Import at_borrow.
 From lrust.typing Require Export type.
 From lrust.typing Require Import typing option.
 
-From gpfsl.gps Require Import middleware protocols escrows.
-
 Set Default Proof Using "Type".
 
 Definition arcN := lrustN .@ "arc".
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index b0ffc6abbbfe7321ff6f6b3342771532e23957d4..f351f1dd0490a3c2f6883d0ba584658d78596fdb 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -6,6 +6,8 @@ From lrust.typing Require Export type.
 From lrust.typing Require Import typing option.
 Set Default Proof Using "Type".
 
+Unset Printing Notations.
+
 Definition rc_stR :=
   prodUR (optionUR (csumR (prodR fracR positiveR) (exclR unitO))) natUR.
 Class rcG Σ :=
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index 06fc0cbb54f3502d2d9806def96a3efe1c70637f..3da2f344df209886afb0e601f75de3e79c1b4a2a 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -1,10 +1,10 @@
 From Coq.QArith Require Import Qcanon.
+From iris.bi Require Import fractional.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth excl csum frac agree.
-From iris.bi Require Import fractional.
+From gpfsl.gps Require Import middleware protocols.
 From lrust.lifetime Require Import at_borrow.
 From lrust.typing Require Import typing.
-From gpfsl.gps Require Import middleware protocols.
 From lrust.logic Require Import gps.
 Set Default Proof Using "Type".
 
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index 3d29bd596ce936b6be19ee2ec38650d82222ac99..9c66a0550e0897e3ee4d10cffe8c95dbcc9349c3 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -1,12 +1,12 @@
+From iris.bi Require Import fractional.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth csum frac agree.
-From iris.bi Require Import fractional.
+From gpfsl.gps Require Import middleware protocols.
+From lrust.logic Require Import gps.
 From lrust.lang Require Import memcpy.
 From lrust.lifetime Require Import at_borrow.
 From lrust.typing Require Import typing option.
 From lrust.typing.lib.rwlock Require Import rwlock rwlockreadguard rwlockwriteguard.
-From gpfsl.gps Require Import middleware protocols.
-From lrust.logic Require Import gps.
 Set Default Proof Using "Type".
 
 (** SYNCHRONIZATION CONDITIONS of rwlock *)
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index a1d00eb5bda63188910de1ee60d950da1b8bac36..aae742a91e79885aaa3382e8878381232002fce1 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -1,12 +1,12 @@
 From Coq.QArith Require Import Qcanon.
+From iris.bi Require Import fractional.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth csum frac agree.
-From iris.bi Require Import fractional.
+From gpfsl.gps Require Import middleware protocols.
+From lrust.logic Require Import gps.
 From lrust.lifetime Require Import at_borrow.
 From lrust.typing Require Import typing.
 From lrust.typing.lib.rwlock Require Import rwlock rwlockreadguard.
-From gpfsl.gps Require Import middleware protocols.
-From lrust.logic Require Import gps.
 Set Default Proof Using "Type".
 
 Section rwlockreadguard_functions.
@@ -161,7 +161,7 @@ Section rwlockreadguard_functions.
                 tctx_hasty_val' //=; simpl.
         iFrame "Hx". iExists _,_,_,_. iFrame "Hx' Hαβ Hν H◯ H†".
         iExists _,_,_. iSplitL "R''".
-        - iExists _,_; by iDestruct "R''" as "[$ ?]". 
+        - iExists _,_; by iDestruct "R''" as "[$ ?]".
         - iFrame "EqO EqS". iExists _,_. by iFrame "R'". }
       iApply type_jump; solve_typing.
   Qed.
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
index 6d0fa49c80be0f9be6026d2a767fda794cc05a7f..4c9a3ca3c51c0e0abdaea98bedb4176019621151 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -1,12 +1,12 @@
 From Coq.QArith Require Import Qcanon.
+From iris.bi Require Import fractional.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth csum frac agree.
-From iris.bi Require Import fractional.
+From gpfsl.gps Require Import middleware.
+From lrust.logic Require Import gps.
 From lrust.lifetime Require Import at_borrow.
 From lrust.typing Require Import typing.
 From lrust.typing.lib.rwlock Require Import rwlock rwlockwriteguard.
-From gpfsl.gps Require Import middleware.
-From lrust.logic Require Import gps.
 Set Default Proof Using "Type".
 
 Section rwlockwriteguard_functions.
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 2be078c81c64fe3c34afe24328889a70c08fda6d..1b3d3a74abdfb5080f3573d25f20eae17e3d50d2 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -1,6 +1,6 @@
 From gpfsl.logic Require Import proofmode.
 From lrust.lang Require Export memcpy.
-From lrust.typing Require Export type lft_contexts type_context cont_context.
+From lrust.typing Require Export lft_contexts type_context cont_context type.
 Set Default Proof Using "Type".
 
 Implicit Types tid : thread_id.