diff --git a/opam b/opam
index 45a8a7a23bfd684dc64f669343e3e13f023b608d..d83a72b7462a1219c3acf9a4a6a292ed41f9667e 100644
--- a/opam
+++ b/opam
@@ -11,5 +11,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
 depends: [
-  "coq-iris" { (= "dev.2019-08-12.2.2dc1c367") | (= "dev") }
+  "coq-iris" { (= "dev.2019-08-13.5.c1d6ef7f") | (= "dev") }
 ]
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index 61343b05857bb79ee92c0c39c11db14935014091..d7ec26143e37de25724431cb0d7b1f3e76de009c 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -118,7 +118,7 @@ Section heap.
   Global Instance heap_mapsto_fractional l v: Fractional (λ q, l ↦{q} v)%I.
   Proof.
     intros p q.
-    by rewrite heap_mapsto_eq -own_op -auth_frag_op op_singleton pair_op agree_idemp.
+    by rewrite heap_mapsto_eq -own_op -auth_frag_op op_singleton -pair_op agree_idemp.
   Qed.
   Global Instance heap_mapsto_as_fractional l q v:
     AsFractional (l ↦{q} v) (λ q, l ↦{q} v)%I q.
@@ -143,7 +143,7 @@ Section heap.
   Proof.
     rewrite heap_mapsto_eq -own_op -auth_frag_op own_valid discrete_valid.
     eapply pure_elim; [done|]=> /auth_frag_valid /=.
-    rewrite op_singleton pair_op singleton_valid=> -[? /agree_op_invL'->]; eauto.
+    rewrite op_singleton -pair_op singleton_valid=> -[? /agree_op_invL'->]; eauto.
   Qed.
 
   Lemma heap_mapsto_vec_nil l q : l ↦∗{q} [] ⊣⊢ True.
@@ -272,7 +272,7 @@ Section heap.
     †{q1}l…n ∗ †{q2}l+ₗn … n' ⊣⊢ †{q1+q2}l…(n+n').
   Proof.
     by rewrite heap_freeable_eq /heap_freeable_def -own_op -auth_frag_op
-      op_singleton pair_op inter_op.
+      op_singleton -pair_op inter_op.
   Qed.
 
   (** Properties about heap_freeable_rel and heap_freeable *)
diff --git a/theories/lang/lib/arc.v b/theories/lang/lib/arc.v
index b257e89e6f4c8b88f841dde741dd94df9e96a680..5ed568efc3e43cd88443b097414b982069eb4077 100644
--- a/theories/lang/lib/arc.v
+++ b/theories/lang/lib/arc.v
@@ -527,7 +527,7 @@ Section arc.
         iApply ("HΦ"). rewrite -{2}Hq''. iFrame. by iApply close_last_strong.
       + destruct Hqq' as [? ->].
         rewrite -[in (_, _)](Pos.succ_pred s) // -[wl in Cinl (_, wl)]left_id
-                -Pos.add_1_l -2!pair_op -Cinl_op Some_op.
+                -Pos.add_1_l 2!pair_op Cinl_op Some_op.
         iMod (own_update_2 _ _ _ _ with "H● Hown") as "H●".
         { apply auth_update_dealloc, prod_local_update_1, @cancel_local_update_unit, _. }
         iMod ("Hclose" with "[- HΦ]") as "_".
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 6d16148d07d1f843c3bb8fe0af54602572c2cb0b..377a8108b689d949607194147f7f92234fb20633 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -290,7 +290,7 @@ Proof. rewrite /lft_dead. iDestruct 1 as (Λ) "[% H']". set_solver. Qed.
 Global Instance lft_tok_fractional κ : Fractional (λ q, q.[κ])%I.
 Proof.
   intros p q. rewrite /lft_tok -big_sepMS_sep. apply big_sepMS_proper.
-  intros Λ ?. rewrite -Cinl_op -op_singleton auth_frag_op own_op //.
+  intros Λ ?. rewrite Cinl_op -op_singleton auth_frag_op own_op //.
 Qed.
 Global Instance lft_tok_as_fractional κ q :
   AsFractional q.[κ] (λ q, q.[κ])%I q.
@@ -298,7 +298,7 @@ Proof. split. done. apply _. Qed.
 Global Instance idx_bor_own_fractional i : Fractional (λ q, idx_bor_own q i)%I.
 Proof.
   intros p q. rewrite /idx_bor_own -own_bor_op /own_bor. f_equiv=>?.
-  rewrite -auth_frag_op op_singleton pair_op agree_idemp. done.
+  rewrite -auth_frag_op op_singleton -pair_op agree_idemp. done.
 Qed.
 Global Instance idx_bor_own_as_fractional i q :
   AsFractional (idx_bor_own q i) (λ q, idx_bor_own q i)%I q.
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 43a941772aacfa609549545fafff960131113351..67f16b8db67df6129331d10a09048d48067b0e21 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -365,7 +365,7 @@ Section code.
           iFrame. iExists _. iFrame. auto with iFrame.
         * iMod (own_update_2 with "Hst Htok") as "Hst".
           { apply auth_update_dealloc.
-            rewrite -pair_op -Cinl_op Some_op -{1}(left_id 0%nat _ weak) -pair_op.
+            rewrite pair_op Cinl_op Some_op -{1}(left_id 0%nat _ weak) pair_op.
             apply (cancel_local_update_unit _ (_, _)). }
           iApply "Hclose". iFrame. iExists _. iFrame. iExists (q+q'')%Qp. iFrame.
           iSplitL; first last.
@@ -585,7 +585,7 @@ Section code.
       split; simpl; last done. apply frac_valid'. rewrite -H comm_L -{2}(Qp_div_2 qb).
       apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (_ / _)%Qp).
       apply Qcplus_le_mono_r, Qp_ge_0. }
-    rewrite right_id -Some_op Cinl_op pair_op. iDestruct "Hνtok" as "[Hνtok1 Hνtok2]".
+    rewrite right_id -Some_op -Cinl_op -pair_op. iDestruct "Hνtok" as "[Hνtok1 Hνtok2]".
     iMod ("Hclose3" with "[$Hrctok] Hna") as "[Hα1 Hna]".
     iMod ("Hclose2" with "[Hrc● Hl'1 Hl'2 Hl'† Hνtok2 Hν† $Hna]") as "Hna".
     { iExists _. iFrame "Hrc●". iExists _. rewrite Z.add_comm. iFrame.
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index 230bbf11468dad4103d96e6bb7255f49d1abf50b..f9cfc80c90501aa5b4d7fa334c285d6661a36b35 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -172,7 +172,7 @@ Section code.
         rewrite -Hq''q0 comm_L -{2}(Qp_div_2 qb).
         apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (_ / _)%Qp).
         apply Qcplus_le_mono_r, Qp_ge_0. }
-      rewrite right_id -Some_op Cinl_op pair_op.
+      rewrite right_id -Some_op -Cinl_op -pair_op.
       iMod ("Hclose3" with "[$Hwtok] Hna") as "[Hα1 Hna]".
       iMod ("Hclose2" with "[Hrc● Hl'1 Hl'2 Hl'† Hν2 Hν† $Hna]") as "Hna".
       { iExists _. iFrame "Hrc●". iExists _. rewrite Z.add_comm. iFrame.
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index 35d2901d534d21887080156fe22e67f386b7adb9..14f5aa39e914acd6270a5e70e94a5115646e50f0 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -83,7 +83,7 @@ Section ref_functions.
     wp_let. wp_apply (wp_memcpy with "[$Hlr $H↦]"); [done..|].
     iIntros "[Hlr H↦]". wp_seq. iMod ("Hcloseα2" with "[$H◯] Hna") as "[Hα1 Hna]".
     iMod ("Hcloseδ" with "[H↦lrc H● Hν1 Hshr' H†] Hna") as "[Hδ Hna]".
-    { iExists (Some (_, false, _, _)). rewrite Z.add_comm -Some_op !pair_op agree_idemp.
+    { iExists (Some (_, false, _, _)). rewrite Z.add_comm -Some_op -!pair_op agree_idemp.
       iFrame. iExists _. iFrame.
       rewrite (comm Qp_plus) (assoc Qp_plus) Qp_div_2 (comm Qp_plus). auto. }
     iMod ("Hcloseβ" with "Hδ") as "Hβ". iMod ("Hcloseα1" with "[$H↦]") as "Hα2".
@@ -178,7 +178,7 @@ Section ref_functions.
           by rewrite Pos.add_1_l Pos.pred_succ. }
         iMod (own_update with "H●◯") as "$".
         { apply auth_update_dealloc.
-          rewrite -(agree_idemp (to_agree _)) -!pair_op Some_op.
+          rewrite -(agree_idemp (to_agree _)) !pair_op Some_op.
           apply (cancel_local_update_unit (reading_stR q ν)), _. }
         iApply step_fupd_intro; first set_solver. iExists (q+q'')%Qp. iFrame.
         by rewrite assoc (comm _ q0 q). }
@@ -349,7 +349,7 @@ Section ref_functions.
     iDestruct "Hrefs" as "(Hrefs1 & Hrefs2 & Hrefs3 & Hrefs4)".
     rewrite !shift_loc_assoc. wp_write. do 3 (wp_op; wp_write).
     iMod ("Hclosena" with "[H↦lrc H● Hν1 Hshr' H†] Hna") as "[Hβ Hna]".
-    { iExists (Some (_, false, _, _)). rewrite Z.add_comm -Some_op !pair_op agree_idemp.
+    { iExists (Some (_, false, _, _)). rewrite Z.add_comm -Some_op -!pair_op agree_idemp.
       iFrame. iExists _. iFrame.
       rewrite (comm Qp_plus) (assoc Qp_plus) Qp_div_2 (comm Qp_plus). auto. }
     iMod ("Hβclose" with "Hβ") as "Hα". iMod ("Hclose1" with "Hα HL") as "HL".
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index a70435daeeea57c643fc82552c3f9fd724724f4b..a480a68a23b10f45f6a5e624f4262bc271f156a7 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -190,7 +190,7 @@ Section refcell_functions.
               apply Qcplus_le_mono_r, Qp_ge_0.
             - done. }
           iFrame "∗#". iExists (Some (ν, false, _, _)). iFrame "∗#".
-          rewrite [_ â‹… _]comm -Some_op !pair_op agree_idemp. iFrame.
+          rewrite [_ â‹… _]comm -Some_op -!pair_op agree_idemp. iFrame.
           iExists _. iFrame. rewrite -(assoc Qp_plus) Qp_div_2 //.
         - iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]". done.
           iMod (own_update with "Hownst") as "[Hownst Hreading]"; first by apply
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index 43e251302e8a45789ff301d142f5b703b117102f..ae82ed434946c89d54f94ce48a7049969d49f3b7 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -143,7 +143,7 @@ Section refmut_functions.
         iDestruct "Hq" as (q) "(<- & ?)". iFrame.
       - simpl in *. setoid_subst. iExists (Some (_, _, _, _)).
         iMod (own_update_2 with "H● H◯") as "$".
-        { apply auth_update_dealloc. rewrite -(agree_idemp (to_agree _)) -!pair_op Some_op.
+        { apply auth_update_dealloc. rewrite -(agree_idemp (to_agree _)) !pair_op Some_op.
           apply (cancel_local_update_unit (writing_stR q _)), _. }
         iDestruct "INV" as "(H† & Hq & _)".
         rewrite /= (_:Z.neg (1%positive â‹… n') + 1 = Z.neg n');
@@ -322,7 +322,7 @@ Section refmut_functions.
     rewrite !shift_loc_assoc. wp_write. do 3 (wp_op; wp_write).
     iMod ("Hclosena" with "[Hlrc H● Hν1 H†] Hna") as "[Hβ Hna]".
     { iExists (Some (_, true, _, _)).
-      rewrite -Some_op !pair_op agree_idemp /= (comm _ xH _).
+      rewrite -Some_op -!pair_op agree_idemp /= (comm _ xH _).
       iFrame. iSplitL; [|done]. iExists _. iFrame.
       rewrite (comm Qp_plus) (assoc Qp_plus) Qp_div_2 (comm Qp_plus). auto. }
     iMod ("Hβclose" with "Hβ") as "Hα". iMod ("Hclose1" with "Hα HL") as "HL".
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index 0cca47c4e3af7cbfcea498e45b50da2af0164b44..2cb00ca6197b2df501d722a7a86031c4f07769b1 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -117,7 +117,7 @@ Section rwlockreadguard_functions.
           iApply (own_update_2 with "H● H◯"). apply auth_update_dealloc.
           assert (n = 1%positive â‹… Pos.pred n) as EQn.
           { rewrite pos_op_plus -Pplus_one_succ_l Pos.succ_pred // =>?. by subst. }
-          rewrite {1}EQn -{1}(agree_idemp (to_agree _)) -2!pair_op -Cinr_op Some_op.
+          rewrite {1}EQn -{1}(agree_idemp (to_agree _)) 2!pair_op Cinr_op Some_op.
           apply (cancel_local_update_unit (reading_st q ν)) , _. }
       iApply (wp_step_fupd with "INV"). done. set_solver.
       iApply (wp_cas_int_suc with "Hlx"); try done. iNext. iIntros "Hlx INV !>".