diff --git a/opam b/opam
index 1e75e2c215ff3fe089cff1feae1eef4b0b5e9223..36332e3acd7eba971dac4caa07a7e5b9512cdd96 100644
--- a/opam
+++ b/opam
@@ -16,7 +16,7 @@ This branch uses a proper weak memory model.
 """
 
 depends: [
-  "coq-gpfsl" { (= "dev.2020-09-06.0.570c82c9") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2020-09-15.0.f118e18e") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lang/arc_cmra.v b/theories/lang/arc_cmra.v
index 07ec46d14c9fbefe0ca963312f77d2a6ef669e67..ce111fe8d0b2244637bd8fdb812f1b79fe98a0d9 100644
--- a/theories/lang/arc_cmra.v
+++ b/theories/lang/arc_cmra.v
@@ -220,7 +220,7 @@ Section ArcGhost.
     iIntros "own". iDestruct (own_valid with "own") as %VAL. iPureIntro.
     move : VAL => [/=_ [/= [[VAL  _]_]_]]. move :VAL.
     rewrite /= -auth_frag_op -Some_op -pair_op auth_valid_discrete /= Some_valid.
-    move => [_ /agree_op_inv' /to_latT_inj /leibniz_equiv_iff // ].
+    move => [_ /to_agree_op_inv /to_latT_inj /leibniz_equiv_iff // ].
   Qed.
 
   Lemma StrongMoveAuth_Cert_include γ Mt Mt':
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index bcda1f20c066dcb3d1a0e2ecf3dc19b65d71e835..fb9343ca3971cd1f3a6665b972252cef90ba1b75 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -70,7 +70,7 @@ Proof.
   iIntros "[Hx Hy]".
   iDestruct "Hx" as (γs) "[Hγs Hx]"; iDestruct "Hy" as (γs') "[Hγs' Hy]".
   iDestruct (own_valid_2 with "Hγs Hγs'") as %Hγs. move : Hγs.
-  rewrite auth_frag_valid singleton_op singleton_valid=> /agree_op_invL' <-.
+  rewrite auth_frag_valid singleton_op singleton_valid=> /to_agree_op_inv_L <-.
   iExists γs. iSplit. done. rewrite own_op; iFrame.
 Qed.
 Global Instance own_bor_into_sep κ x x1 x2 :
@@ -102,7 +102,7 @@ Proof.
   iIntros "[Hx Hy]".
   iDestruct "Hx" as (γs) "[Hγs Hx]"; iDestruct "Hy" as (γs') "[Hγs' Hy]".
   iDestruct (own_valid_2 with "Hγs Hγs'") as %Hγs. move : Hγs.
-  rewrite auth_frag_valid singleton_op singleton_valid=> /agree_op_invL' <-.
+  rewrite auth_frag_valid singleton_op singleton_valid=> /to_agree_op_inv_L <-.
   iExists γs. iSplit; first done. rewrite own_op; iFrame.
 Qed.
 Global Instance own_cnt_into_sep κ x x1 x2 :
@@ -136,7 +136,7 @@ Proof.
   iIntros "[Hx Hy]".
   iDestruct "Hx" as (γs) "[Hγs Hx]"; iDestruct "Hy" as (γs') "[Hγs' Hy]".
   iDestruct (own_valid_2 with "Hγs Hγs'") as %Hγs. move : Hγs.
-  rewrite -auth_frag_op auth_frag_valid singleton_op singleton_valid=> /agree_op_invL' <-.
+  rewrite -auth_frag_op auth_frag_valid singleton_op singleton_valid=> /to_agree_op_inv_L <-.
   iExists γs. iSplit. done. rewrite own_op; iFrame.
 Qed.
 Global Instance own_inh_into_sep κ x x1 x2 :
diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v
index 0622b4126e5ebc09bda751d450b334d10ae86df8..6f79fbc2e0a0c900143f4d243773d0a081c84e01 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -25,7 +25,7 @@ Proof.
   iIntros "(#Hag & Hσ & Hclose)". iSplitL "Hσ"; [by auto|]. iIntros "H".
   iApply "Hclose". iDestruct "H" as (γ') "[#Hag' H]".
   iDestruct (own_valid_2 with "Hag Hag'") as %Hγs. move : Hγs.
-  rewrite auth_frag_valid singleton_op singleton_valid=> /agree_op_invL' <- //.
+  rewrite auth_frag_valid singleton_op singleton_valid=> /to_agree_op_inv_L <- //.
 Qed.
 
 Section reborrow.