diff --git a/ProofMode.md b/ProofMode.md
index b165c01a5cd895cf2126ffd4aff53844e8849312..4e8a1599321c85be80a156960f0daffe31d01a2d 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -111,6 +111,9 @@ Separation logic-specific tactics
   framed.
 - `iCombine "H1" "H2" as "pat"` : combines `H1 : P1` and `H2 : P2` into
   `H: P1 ∗ P2`, then calls `iDestruct H as pat` on the combined hypothesis.
+- `iAccu` : solves a goal that is an evar by instantiating it with a all
+  hypotheses from the spatial context joined together with a separating
+  conjunction (or `emp` in case the spatial context is empty).
 
 Modalities
 ----------
@@ -234,11 +237,13 @@ appear at the top level:
 
 For example, given:
 
-        ∀ x, x = 0 ⊢ □ (P → False ∨ □ (Q ∧ ▷ R) -∗ P ∗ ▷ (R ∗ Q ∧ x = pred 2)).
+        ∀ x, <affine> ⌜ x = 0 ⌝ ⊢
+          □ (P → False ∨ □ (Q ∧ ▷ R) -∗
+          P ∗ ▷ (R ∗ Q ∧ ⌜ x = pred 2 ⌝)).
 
 You can write
 
-        iIntros (x) "% !# $ [[] | #[HQ HR]] /= !>".
+        iIntros (x Hx) "!# $ [[] | #[HQ HR]] /= !>".
 
 which results in:
 
diff --git a/opam b/opam
index 73abcaa5786bfebff6a6fe4431e4b983ed531bb6..6136230fe295edb0a0638d679ee5c0e9e9d18c0c 100644
--- a/opam
+++ b/opam
@@ -11,5 +11,5 @@ install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
 depends: [
   "coq" { (>= "8.7.1" & < "8.10~") | (= "dev") }
-  "coq-stdpp" { (= "dev.2019-03-26.0.d98ab4e4") | (= "dev") }
+  "coq-stdpp" { (= "dev.2019-04-26.2.32eab16e") | (= "dev") }
 ]
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index d4418c515e2d989ff513ce006dfa32448a8228e1..9df5355cdbeb3e6c4b00ef2fa4a87edc34bf9fe7 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -45,21 +45,21 @@ Section mixin.
   Record CmraMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, ValidN A} := {
     (* setoids *)
     mixin_cmra_op_ne (x : A) : NonExpansive (op x);
-    mixin_cmra_pcore_ne n x y cx :
+    mixin_cmra_pcore_ne n (x y : A) cx :
       x ≡{n}≡ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≡{n}≡ cy;
     mixin_cmra_validN_ne n : Proper (dist n ==> impl) (validN n);
     (* valid *)
-    mixin_cmra_valid_validN x : ✓ x ↔ ∀ n, ✓{n} x;
-    mixin_cmra_validN_S n x : ✓{S n} x → ✓{n} x;
+    mixin_cmra_valid_validN (x : A) : ✓ x ↔ ∀ n, ✓{n} x;
+    mixin_cmra_validN_S n (x : A) : ✓{S n} x → ✓{n} x;
     (* monoid *)
-    mixin_cmra_assoc : Assoc (≡) (⋅);
-    mixin_cmra_comm : Comm (≡) (⋅);
-    mixin_cmra_pcore_l x cx : pcore x = Some cx → cx ⋅ x ≡ x;
-    mixin_cmra_pcore_idemp x cx : pcore x = Some cx → pcore cx ≡ Some cx;
-    mixin_cmra_pcore_mono x y cx :
+    mixin_cmra_assoc : Assoc (≡@{A}) (⋅);
+    mixin_cmra_comm : Comm (≡@{A}) (⋅);
+    mixin_cmra_pcore_l (x : A) cx : pcore x = Some cx → cx ⋅ x ≡ x;
+    mixin_cmra_pcore_idemp (x : A) cx : pcore x = Some cx → pcore cx ≡ Some cx;
+    mixin_cmra_pcore_mono (x y : A) cx :
       x ≼ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≼ cy;
-    mixin_cmra_validN_op_l n x y : ✓{n} (x ⋅ y) → ✓{n} x;
-    mixin_cmra_extend n x y1 y2 :
+    mixin_cmra_validN_op_l n (x y : A) : ✓{n} (x ⋅ y) → ✓{n} x;
+    mixin_cmra_extend n (x y1 y2 : A) :
       ✓{n} x → x ≡{n}≡ y1 ⋅ y2 →
       { z1 : A & { z2 | x ≡ z1 ⋅ z2 ∧ z1 ≡{n}≡ y1 ∧ z2 ≡{n}≡ y2 } }
   }.
@@ -187,7 +187,7 @@ Class Unit (A : Type) := ε : A.
 Arguments ε {_ _}.
 
 Record UcmraMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, Unit A} := {
-  mixin_ucmra_unit_valid : ✓ ε;
+  mixin_ucmra_unit_valid : ✓ (ε : A);
   mixin_ucmra_unit_left_id : LeftId (≡) ε (⋅);
   mixin_ucmra_pcore_unit : pcore ε ≡ Some ε
 }.
@@ -861,17 +861,17 @@ End cmra_transport.
 Record RAMixin A `{Equiv A, PCore A, Op A, Valid A} := {
   (* setoids *)
   ra_op_proper (x : A) : Proper ((≡) ==> (≡)) (op x);
-  ra_core_proper x y cx :
+  ra_core_proper (x y : A) cx :
     x ≡ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≡ cy;
-  ra_validN_proper : Proper ((≡) ==> impl) valid;
+  ra_validN_proper : Proper ((≡@{A}) ==> impl) valid;
   (* monoid *)
-  ra_assoc : Assoc (≡) (⋅);
-  ra_comm : Comm (≡) (⋅);
-  ra_pcore_l x cx : pcore x = Some cx → cx ⋅ x ≡ x;
-  ra_pcore_idemp x cx : pcore x = Some cx → pcore cx ≡ Some cx;
-  ra_pcore_mono x y cx :
+  ra_assoc : Assoc (≡@{A}) (⋅);
+  ra_comm : Comm (≡@{A}) (⋅);
+  ra_pcore_l (x : A) cx : pcore x = Some cx → cx ⋅ x ≡ x;
+  ra_pcore_idemp (x : A) cx : pcore x = Some cx → pcore cx ≡ Some cx;
+  ra_pcore_mono (x y : A) cx :
     x ≼ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≼ cy;
-  ra_valid_op_l x y : ✓ (x ⋅ y) → ✓ x
+  ra_valid_op_l (x y : A) : ✓ (x ⋅ y) → ✓ x
 }.
 
 Section discrete.
@@ -1491,7 +1491,7 @@ Proof.
   by intros ? A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, rFunctor_contractive.
 Qed.
 
-(* Dependently-typed functions over a finite discrete domain *)
+(* Dependently-typed functions over a discrete domain *)
 Section ofe_fun_cmra.
   Context `{B : A → ucmraT}.
   Implicit Types f g : ofe_fun B.
diff --git a/theories/algebra/dra.v b/theories/algebra/dra.v
index a7f7ee7430a91bbf5f07ee091b0469f4ee93edcc..8f65c8eb7c937810c28fec208e4366ab718d370c 100644
--- a/theories/algebra/dra.v
+++ b/theories/algebra/dra.v
@@ -3,26 +3,27 @@ Set Default Proof Using "Type".
 
 Record DraMixin A `{Equiv A, Core A, Disjoint A, Op A, Valid A} := {
   (* setoids *)
-  mixin_dra_equivalence : Equivalence ((≡) : relation A);
-  mixin_dra_op_proper : Proper ((≡) ==> (≡) ==> (≡)) (⋅);
-  mixin_dra_core_proper : Proper ((≡) ==> (≡)) core;
-  mixin_dra_valid_proper : Proper ((≡) ==> impl) valid;
-  mixin_dra_disjoint_proper x : Proper ((≡) ==> impl) (disjoint x);
+  mixin_dra_equivalence : Equivalence (≡@{A});
+  mixin_dra_op_proper : Proper ((≡@{A}) ==> (≡) ==> (≡)) (⋅);
+  mixin_dra_core_proper : Proper ((≡@{A}) ==> (≡)) core;
+  mixin_dra_valid_proper : Proper ((≡@{A}) ==> impl) valid;
+  mixin_dra_disjoint_proper (x : A) : Proper ((≡) ==> impl) (disjoint x);
   (* validity *)
-  mixin_dra_op_valid x y : ✓ x → ✓ y → x ## y → ✓ (x ⋅ y);
-  mixin_dra_core_valid x : ✓ x → ✓ core x;
+  mixin_dra_op_valid (x y : A) : ✓ x → ✓ y → x ## y → ✓ (x ⋅ y);
+  mixin_dra_core_valid (x : A) : ✓ x → ✓ core x;
   (* monoid *)
-  mixin_dra_assoc x y z :
+  mixin_dra_assoc (x y z : A) :
     ✓ x → ✓ y → ✓ z → x ## y → x ⋅ y ## z → x ⋅ (y ⋅ z) ≡ (x ⋅ y) ⋅ z;
-  mixin_dra_disjoint_ll x y z : ✓ x → ✓ y → ✓ z → x ## y → x ⋅ y ## z → x ## z;
-  mixin_dra_disjoint_move_l x y z :
+  mixin_dra_disjoint_ll (x y z :  A) :
+    ✓ x → ✓ y → ✓ z → x ## y → x ⋅ y ## z → x ## z;
+  mixin_dra_disjoint_move_l (x y z : A) :
     ✓ x → ✓ y → ✓ z → x ## y → x ⋅ y ## z → x ## y ⋅ z;
   mixin_dra_symmetric : Symmetric (@disjoint A _);
-  mixin_dra_comm x y : ✓ x → ✓ y → x ## y → x ⋅ y ≡ y ⋅ x;
-  mixin_dra_core_disjoint_l x : ✓ x → core x ## x;
-  mixin_dra_core_l x : ✓ x → core x ⋅ x ≡ x;
-  mixin_dra_core_idemp x : ✓ x → core (core x) ≡ core x;
-  mixin_dra_core_mono x y :
+  mixin_dra_comm (x y : A) : ✓ x → ✓ y → x ## y → x ⋅ y ≡ y ⋅ x;
+  mixin_dra_core_disjoint_l (x : A) : ✓ x → core x ## x;
+  mixin_dra_core_l (x : A) : ✓ x → core x ⋅ x ≡ x;
+  mixin_dra_core_idemp (x : A) : ✓ x → core (core x) ≡ core x;
+  mixin_dra_core_mono (x y : A) :
     ∃ z, ✓ x → ✓ y → x ## y → core (x ⋅ y) ≡ core x ⋅ z ∧ ✓ z ∧ core x ## z
 }.
 Structure draT := DraT {
diff --git a/theories/bi/embedding.v b/theories/bi/embedding.v
index b5ee8ae509a4ca3ca66f947e13c0b1332dcf7715..a0b19edb8cf739934ec25b19c85076e63e32b32c 100644
--- a/theories/bi/embedding.v
+++ b/theories/bi/embedding.v
@@ -12,17 +12,23 @@ Hint Mode Embed - ! : typeclass_instances.
 
 (* Mixins allow us to create instances easily without having to use Program *)
 Record BiEmbedMixin (PROP1 PROP2 : bi) `(Embed PROP1 PROP2) := {
-  bi_embed_mixin_ne : NonExpansive embed;
-  bi_embed_mixin_mono : Proper ((⊢) ==> (⊢)) embed;
+  bi_embed_mixin_ne : NonExpansive (embed (A:=PROP1) (B:=PROP2));
+  bi_embed_mixin_mono : Proper ((⊢) ==> (⊢)) (embed (A:=PROP1) (B:=PROP2));
   bi_embed_mixin_emp_valid_inj (P : PROP1) :
     bi_emp_valid (PROP:=PROP2) ⎡P⎤ → bi_emp_valid P;
-  bi_embed_mixin_emp_2 : emp ⊢ ⎡emp⎤;
-  bi_embed_mixin_impl_2 P Q : (⎡P⎤ → ⎡Q⎤) ⊢ ⎡P → Q⎤;
-  bi_embed_mixin_forall_2 A (Φ : A → PROP1) : (∀ x, ⎡Φ x⎤) ⊢ ⎡∀ x, Φ x⎤;
-  bi_embed_mixin_exist_1 A (Φ : A → PROP1) : ⎡∃ x, Φ x⎤ ⊢ ∃ x, ⎡Φ x⎤;
-  bi_embed_mixin_sep P Q : ⎡P ∗ Q⎤ ⊣⊢ ⎡P⎤ ∗ ⎡Q⎤;
-  bi_embed_mixin_wand_2 P Q : (⎡P⎤ -∗ ⎡Q⎤) ⊢ ⎡P -∗ Q⎤;
-  bi_embed_mixin_persistently P : ⎡<pers> P⎤ ⊣⊢ <pers> ⎡P⎤
+  bi_embed_mixin_emp_2 : emp ⊢@{PROP2} ⎡emp⎤;
+  bi_embed_mixin_impl_2 (P Q : PROP1) :
+    (⎡P⎤ → ⎡Q⎤) ⊢@{PROP2} ⎡P → Q⎤;
+  bi_embed_mixin_forall_2 A (Φ : A → PROP1) :
+    (∀ x, ⎡Φ x⎤) ⊢@{PROP2} ⎡∀ x, Φ x⎤;
+  bi_embed_mixin_exist_1 A (Φ : A → PROP1) :
+    ⎡∃ x, Φ x⎤ ⊢@{PROP2} ∃ x, ⎡Φ x⎤;
+  bi_embed_mixin_sep (P Q : PROP1) :
+    ⎡P ∗ Q⎤ ⊣⊢@{PROP2} ⎡P⎤ ∗ ⎡Q⎤;
+  bi_embed_mixin_wand_2 (P Q : PROP1) :
+    (⎡P⎤ -∗ ⎡Q⎤) ⊢@{PROP2} ⎡P -∗ Q⎤;
+  bi_embed_mixin_persistently (P : PROP1) :
+    ⎡<pers> P⎤ ⊣⊢@{PROP2} <pers> ⎡P⎤
 }.
 
 Class BiEmbed (PROP1 PROP2 : bi) := {
@@ -302,7 +308,8 @@ Section sbi_embed.
     ⎡■?p P⎤ ⊢ ■?p ⎡P⎤.
   Proof. destruct p; simpl; auto using embed_plainly_1. Qed.
 
-  Lemma embed_plain `{!BiPlainly PROP1, !BiPlainly PROP2} P : Plain P → Plain ⎡P⎤.
+  Lemma embed_plain `{!BiPlainly PROP1, !BiPlainly PROP2} (P : PROP1) :
+    Plain P → Plain (PROP:=PROP2) ⎡P⎤.
   Proof. intros ?. by rewrite /Plain {1}(plain P) embed_plainly_1. Qed.
 
   Global Instance embed_timeless P : Timeless P → Timeless ⎡P⎤.
diff --git a/theories/bi/lib/atomic.v b/theories/bi/lib/atomic.v
index 906de8a56c0641154a5787569217fc087884b10c..bcfc613bc11b66dbe7ba73c3a08c3e23d57d5f16 100644
--- a/theories/bi/lib/atomic.v
+++ b/theories/bi/lib/atomic.v
@@ -288,7 +288,7 @@ Section lemmas.
     rewrite atomic_update_eq {1}/atomic_update_def /=.
     iIntros (??? HAU) "[#HP HQ]".
     iApply (greatest_fixpoint_coind _ (λ _, Q)); last done. iIntros "!#" ([]) "HQ".
-    iApply (make_laterable_intro with "[] HQ"). iIntros "!# >HQ".
+    iApply (make_laterable_intro Q with "[] HQ"). iIntros "!# >HQ".
     iApply HAU. by iFrame.
   Qed.
 
diff --git a/theories/bi/lib/fractional.v b/theories/bi/lib/fractional.v
index cef06cc0fc7390801b3c8d5bd30df045fce918a8..0223efdce9a9ae59e8aae3ba57cf7501675526aa 100644
--- a/theories/bi/lib/fractional.v
+++ b/theories/bi/lib/fractional.v
@@ -30,11 +30,11 @@ Section fractional.
   Lemma fractional_split_1 P P1 P2 Φ q1 q2 :
     AsFractional P Φ (q1 + q2) → AsFractional P1 Φ q1 → AsFractional P2 Φ q2 →
     P -∗ P1 ∗ P2.
-  Proof. intros. by rewrite -fractional_split. Qed.
+  Proof. intros. by rewrite -(fractional_split P). Qed.
   Lemma fractional_split_2 P P1 P2 Φ q1 q2 :
     AsFractional P Φ (q1 + q2) → AsFractional P1 Φ q1 → AsFractional P2 Φ q2 →
     P1 -∗ P2 -∗ P.
-  Proof. intros. apply bi.wand_intro_r. by rewrite -fractional_split. Qed.
+  Proof. intros. apply bi.wand_intro_r. by rewrite -(fractional_split P). Qed.
 
   Lemma fractional_half P P12 Φ q :
     AsFractional P Φ q → AsFractional P12 Φ (q/2) →
@@ -43,11 +43,11 @@ Section fractional.
   Lemma fractional_half_1 P P12 Φ q :
     AsFractional P Φ q → AsFractional P12 Φ (q/2) →
     P -∗ P12 ∗ P12.
-  Proof. intros. by rewrite -fractional_half. Qed.
+  Proof. intros. by rewrite -(fractional_half P). Qed.
   Lemma fractional_half_2 P P12 Φ q :
     AsFractional P Φ q → AsFractional P12 Φ (q/2) →
     P12 -∗ P12 -∗ P.
-  Proof. intros. apply bi.wand_intro_r. by rewrite -fractional_half. Qed.
+  Proof. intros. apply bi.wand_intro_r. by rewrite -(fractional_half P). Qed.
 
   (** Fractional and logical connectives *)
   Global Instance persistent_fractional P :
diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index 855914c3b4d674c9e711da8011e91b8c6f9a2fde..d69656d034a8b6fadf3ddcd7fa305749325a6a04 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -7,7 +7,7 @@ Structure biIndex :=
     { bi_index_type :> Type;
       bi_index_inhabited : Inhabited bi_index_type;
       bi_index_rel : SqSubsetEq bi_index_type;
-      bi_index_rel_preorder : PreOrder (⊑) }.
+      bi_index_rel_preorder : PreOrder (⊑@{bi_index_type}) }.
 Existing Instances bi_index_inhabited bi_index_rel bi_index_rel_preorder.
 
 (* We may want to instantiate monPred with the reflexivity relation in
diff --git a/theories/bi/plainly.v b/theories/bi/plainly.v
index 2b35de218db4de6ad572fba8b6b731980127712f..b28934bcb2ee6d1e4d2bbbd40f675c5b4579b482 100644
--- a/theories/bi/plainly.v
+++ b/theories/bi/plainly.v
@@ -9,11 +9,11 @@ Notation "â–  P" := (plainly P) : bi_scope.
 
 (* Mixins allow us to create instances easily without having to use Program *)
 Record BiPlainlyMixin (PROP : sbi) `(Plainly PROP) := {
-  bi_plainly_mixin_plainly_ne : NonExpansive plainly;
+  bi_plainly_mixin_plainly_ne : NonExpansive (plainly (A:=PROP));
 
-  bi_plainly_mixin_plainly_mono P Q : (P ⊢ Q) → ■ P ⊢ ■ Q;
-  bi_plainly_mixin_plainly_elim_persistently P : ■ P ⊢ <pers> P;
-  bi_plainly_mixin_plainly_idemp_2 P : ■ P ⊢ ■ ■ P;
+  bi_plainly_mixin_plainly_mono (P Q : PROP) : (P ⊢ Q) → ■ P ⊢ ■ Q;
+  bi_plainly_mixin_plainly_elim_persistently (P : PROP) : ■ P ⊢ <pers> P;
+  bi_plainly_mixin_plainly_idemp_2 (P : PROP) : ■ P ⊢ ■ ■ P;
 
   bi_plainly_mixin_plainly_forall_2 {A} (Ψ : A → PROP) :
     (∀ a, ■ (Ψ a)) ⊢ ■ (∀ a, Ψ a);
@@ -21,17 +21,18 @@ Record BiPlainlyMixin (PROP : sbi) `(Plainly PROP) := {
   (* The following two laws are very similar, and indeed they hold not just
      for persistently and plainly, but for any modality defined as `M P n x :=
      ∀ y, R x y → P n y`. *)
-  bi_plainly_mixin_persistently_impl_plainly P Q :
+  bi_plainly_mixin_persistently_impl_plainly (P Q : PROP) :
     (■ P → <pers> Q) ⊢ <pers> (■ P → Q);
-  bi_plainly_mixin_plainly_impl_plainly P Q : (■ P → ■ Q) ⊢ ■ (■ P → Q);
+  bi_plainly_mixin_plainly_impl_plainly (P Q : PROP) :
+    (■ P → ■ Q) ⊢ ■ (■ P → Q);
 
-  bi_plainly_mixin_plainly_emp_intro P : P ⊢ ■ emp;
-  bi_plainly_mixin_plainly_absorb P Q : ■ P ∗ Q ⊢ ■ P;
+  bi_plainly_mixin_plainly_emp_intro (P : PROP) : P ⊢ ■ emp;
+  bi_plainly_mixin_plainly_absorb (P Q : PROP) : ■ P ∗ Q ⊢ ■ P;
 
-  bi_plainly_mixin_prop_ext P Q : ■ ((P -∗ Q) ∧ (Q -∗ P)) ⊢ P ≡ Q;
+  bi_plainly_mixin_prop_ext (P Q : PROP) : ■ ((P -∗ Q) ∧ (Q -∗ P)) ⊢ P ≡ Q;
 
-  bi_plainly_mixin_later_plainly_1 P : ▷ ■ P ⊢ ■ ▷ P;
-  bi_plainly_mixin_later_plainly_2 P : ■ ▷ P ⊢ ▷ ■ P;
+  bi_plainly_mixin_later_plainly_1 (P : PROP) : ▷ ■ P ⊢ ■ ▷ P;
+  bi_plainly_mixin_later_plainly_2 (P : PROP) : ■ ▷ P ⊢ ▷ ■ P;
 }.
 
 Class BiPlainly (PROP : sbi) := {
diff --git a/theories/bi/updates.v b/theories/bi/updates.v
index 718e153fe7c150e41ed9e9695ef2543b8607da47..5fd78269ad2b3c1a930638531007f5c4d609ef38 100644
--- a/theories/bi/updates.v
+++ b/theories/bi/updates.v
@@ -39,7 +39,7 @@ Notation "P ={ E1 , E2 }▷=∗^ n Q" := (P -∗ |={E1,E2}▷=>^n Q)%I : bi_scop
 (** Bundled versions  *)
 (* Mixins allow us to create instances easily without having to use Program *)
 Record BiBUpdMixin (PROP : bi) `(BUpd PROP) := {
-  bi_bupd_mixin_bupd_ne : NonExpansive bupd;
+  bi_bupd_mixin_bupd_ne : NonExpansive (bupd (PROP:=PROP));
   bi_bupd_mixin_bupd_intro (P : PROP) : P ==∗ P;
   bi_bupd_mixin_bupd_mono (P Q : PROP) : (P ⊢ Q) → (|==> P) ==∗ Q;
   bi_bupd_mixin_bupd_trans (P : PROP) : (|==> |==> P) ==∗ P;
@@ -47,7 +47,7 @@ Record BiBUpdMixin (PROP : bi) `(BUpd PROP) := {
 }.
 
 Record BiFUpdMixin (PROP : sbi) `(FUpd PROP) := {
-  bi_fupd_mixin_fupd_ne E1 E2 : NonExpansive (fupd E1 E2);
+  bi_fupd_mixin_fupd_ne E1 E2 : NonExpansive (fupd (PROP:=PROP) E1 E2);
   bi_fupd_mixin_fupd_intro_mask E1 E2 (P : PROP) : E2 ⊆ E1 → P ⊢ |={E1,E2}=> |={E2,E1}=> P;
   bi_fupd_mixin_except_0_fupd E1 E2 (P : PROP) : ◇ (|={E1,E2}=> P) ={E1,E2}=∗ P;
   bi_fupd_mixin_fupd_mono E1 E2 (P Q : PROP) : (P ⊢ Q) → (|={E1,E2}=> P) ⊢ |={E1,E2}=> Q;
diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index 3cf55913b1c67128b3cc737633adae7140214b56..a8b975d481a95df4b24f2f1f2ae63e9294aa9618 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -1,6 +1,6 @@
 From iris.program_logic Require Export language ectx_language ectxi_language.
 From iris.algebra Require Export ofe.
-From stdpp Require Export strings.
+From stdpp Require Export binders strings.
 From stdpp Require Import gmap.
 Set Default Proof Using "Type".
 
@@ -42,22 +42,6 @@ Inductive bin_op : Set :=
   | ShiftLOp | ShiftROp (* Shifts *)
   | LeOp | LtOp | EqOp. (* Relations *)
 
-Inductive binder := BAnon | BNamed : string → binder.
-Delimit Scope binder_scope with bind.
-Bind Scope binder_scope with binder.
-Definition cons_binder (mx : binder) (X : list string) : list string :=
-  match mx with BAnon => X | BNamed x => x :: X end.
-Infix ":b:" := cons_binder (at level 60, right associativity).
-Instance binder_eq_dec_eq : EqDecision binder.
-Proof. solve_decision. Defined.
-
-Instance set_unfold_cons_binder x mx X P :
-  SetUnfold (x ∈ X) P → SetUnfold (x ∈ mx :b: X) (BNamed x = mx ∨ P).
-Proof.
-  constructor. rewrite -(set_unfold (x ∈ X) P).
-  destruct mx; rewrite /= ?elem_of_cons; naive_solver.
-Qed.
-
 Inductive expr :=
   (* Values *)
   | Val (v : val)
@@ -244,11 +228,6 @@ Proof.
   | 10 => LeOp | 11 => LtOp | _ => EqOp
   end) _); by intros [].
 Qed.
-Instance binder_countable : Countable binder.
-Proof.
- refine (inj_countable' (λ b, match b with BNamed s => Some s | BAnon => None end)
-  (λ b, match b with Some s => BNamed s | None => BAnon end) _); by intros [].
-Qed.
 Instance expr_countable : Countable expr.
 Proof.
  set (enc :=
diff --git a/theories/heap_lang/lib/atomic_heap.v b/theories/heap_lang/lib/atomic_heap.v
index e5d4804bc6b1a592e9c3f40c5f4084e8725b67b0..fd41caa6c2fb8f3e60233485c039ad11248556d7 100644
--- a/theories/heap_lang/lib/atomic_heap.v
+++ b/theories/heap_lang/lib/atomic_heap.v
@@ -19,7 +19,7 @@ Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
   mapsto_fractional l v :> Fractional (λ q, mapsto l q v);
   mapsto_as_fractional l q v :>
     AsFractional (mapsto l q v) (λ q, mapsto l q v) q;
-  mapsto_agree l q1 q2 v1 v2 :> mapsto l q1 v1 -∗ mapsto l q2 v2 -∗ ⌜v1 = v2⌝;
+  mapsto_agree l q1 q2 v1 v2 : mapsto l q1 v1 -∗ mapsto l q2 v2 -∗ ⌜v1 = v2⌝;
   (* -- operation specs -- *)
   alloc_spec (v : val) :
     {{{ True }}} alloc v {{{ l, RET #l; mapsto l 1 v }}};
diff --git a/theories/heap_lang/notation.v b/theories/heap_lang/notation.v
index 81e3fc3e54f5ffb8d3f8b83bd8177d67148096d5..891059ebaae8ceeb99030b4492f888b5d7252bcc 100644
--- a/theories/heap_lang/notation.v
+++ b/theories/heap_lang/notation.v
@@ -15,9 +15,6 @@ Coercion Val : val >-> expr.
 
 Coercion Var : string >-> expr.
 
-Coercion BNamed : string >-> binder.
-Notation "<>" := BAnon : binder_scope.
-
 (* No scope for the values, does not conflict and scope is often not inferred
 properly. *)
 Notation "# l" := (LitV l%Z%V) (at level 8, format "# l").
@@ -50,11 +47,11 @@ Moreover, if the branches do not fit on a single line, it will be printed as:
   end
 *)
 Notation "'match:' e0 'with' 'InjL' x1 => e1 | 'InjR' x2 => e2 'end'" :=
-  (Match e0 x1%bind e1 x2%bind e2)
+  (Match e0 x1%binder e1 x2%binder e2)
   (e0, x1, e1, x2, e2 at level 200,
    format "'[hv' 'match:'  e0  'with'  '/  ' '[' 'InjL'  x1  =>  '/  ' e1 ']'  '/' '[' |  'InjR'  x2  =>  '/  ' e2 ']'  '/' 'end' ']'") : expr_scope.
 Notation "'match:' e0 'with' 'InjR' x1 => e1 | 'InjL' x2 => e2 'end'" :=
-  (Match e0 x2%bind e2 x1%bind e1)
+  (Match e0 x2%binder e2 x1%binder e1)
   (e0, x1, e1, x2, e2 at level 200, only parsing) : expr_scope.
 
 Notation "()" := LitUnit : val_scope.
@@ -81,10 +78,10 @@ Notation "e1 <- e2" := (Store e1%E e2%E) (at level 80) : expr_scope.
 
 (* The breaking point '/  ' makes sure that the body of the rec is indented
 by two spaces in case the whole rec does not fit on a single line. *)
-Notation "'rec:' f x := e" := (Rec f%bind x%bind e%E)
+Notation "'rec:' f x := e" := (Rec f%binder x%binder e%E)
   (at level 200, f at level 1, x at level 1, e at level 200,
    format "'[' 'rec:'  f  x  :=  '/  ' e ']'") : expr_scope.
-Notation "'rec:' f x := e" := (RecV f%bind x%bind e%E)
+Notation "'rec:' f x := e" := (RecV f%binder x%binder e%E)
   (at level 200, f at level 1, x at level 1, e at level 200,
    format "'[' 'rec:'  f  x  :=  '/  ' e ']'") : val_scope.
 Notation "'if:' e1 'then' e2 'else' e3" := (If e1%E e2%E e3%E)
@@ -94,30 +91,30 @@ Notation "'if:' e1 'then' e2 'else' e3" := (If e1%E e2%E e3%E)
 are stated explicitly instead of relying on the Notations Let and Seq as
 defined above. This is needed because App is now a coercion, and these
 notations are otherwise not pretty printed back accordingly. *)
-Notation "'rec:' f x y .. z := e" := (Rec f%bind x%bind (Lam y%bind .. (Lam z%bind e%E) ..))
+Notation "'rec:' f x y .. z := e" := (Rec f%binder x%binder (Lam y%binder .. (Lam z%binder e%E) ..))
   (at level 200, f, x, y, z at level 1, e at level 200,
    format "'[' 'rec:'  f  x  y  ..  z  :=  '/  ' e ']'") : expr_scope.
-Notation "'rec:' f x y .. z := e" := (RecV f%bind x%bind (Lam y%bind .. (Lam z%bind e%E) ..))
+Notation "'rec:' f x y .. z := e" := (RecV f%binder x%binder (Lam y%binder .. (Lam z%binder e%E) ..))
   (at level 200, f, x, y, z at level 1, e at level 200,
    format "'[' 'rec:'  f  x  y  ..  z  :=  '/  ' e ']'") : val_scope.
 
 (* The breaking point '/  ' makes sure that the body of the λ: is indented
 by two spaces in case the whole λ: does not fit on a single line. *)
-Notation "λ: x , e" := (Lam x%bind e%E)
+Notation "λ: x , e" := (Lam x%binder e%E)
   (at level 200, x at level 1, e at level 200,
    format "'[' 'λ:'  x ,  '/  ' e ']'") : expr_scope.
-Notation "λ: x y .. z , e" := (Lam x%bind (Lam y%bind .. (Lam z%bind e%E) ..))
+Notation "λ: x y .. z , e" := (Lam x%binder (Lam y%binder .. (Lam z%binder e%E) ..))
   (at level 200, x, y, z at level 1, e at level 200,
    format "'[' 'λ:'  x  y  ..  z ,  '/  ' e ']'") : expr_scope.
 
-Notation "λ: x , e" := (LamV x%bind e%E)
+Notation "λ: x , e" := (LamV x%binder e%E)
   (at level 200, x at level 1, e at level 200,
    format "'[' 'λ:'  x ,  '/  ' e ']'") : val_scope.
-Notation "λ: x y .. z , e" := (LamV x%bind (Lam y%bind .. (Lam z%bind e%E) .. ))
+Notation "λ: x y .. z , e" := (LamV x%binder (Lam y%binder .. (Lam z%binder e%E) .. ))
   (at level 200, x, y, z at level 1, e at level 200,
    format "'[' 'λ:'  x  y  ..  z ,  '/  ' e ']'") : val_scope.
 
-Notation "'let:' x := e1 'in' e2" := (Lam x%bind e2%E e1%E)
+Notation "'let:' x := e1 'in' e2" := (Lam x%binder e2%E e1%E)
   (at level 200, x at level 1, e1, e2 at level 200,
    format "'[' 'let:'  x  :=  '[' e1 ']'  'in'  '/' e2 ']'") : expr_scope.
 Notation "e1 ;; e2" := (Lam BAnon e2%E e1%E)
@@ -137,10 +134,10 @@ Notation SOME x := (InjR x) (only parsing).
 Notation SOMEV x := (InjRV x) (only parsing).
 
 Notation "'match:' e0 'with' 'NONE' => e1 | 'SOME' x => e2 'end'" :=
-  (Match e0 BAnon e1 x%bind e2)
+  (Match e0 BAnon e1 x%binder e2)
   (e0, e1, x, e2 at level 200, only parsing) : expr_scope.
 Notation "'match:' e0 'with' 'SOME' x => e2 | 'NONE' => e1 'end'" :=
-  (Match e0 BAnon e1 x%bind e2)
+  (Match e0 BAnon e1 x%binder e2)
   (e0, e1, x, e2 at level 200, only parsing) : expr_scope.
 
 Notation "'resolve_proph:' p 'to:' v" := (ResolveProph p v) (at level 100) : expr_scope.
diff --git a/theories/proofmode/class_instances_bi.v b/theories/proofmode/class_instances_bi.v
index c753f95c9f7ec3aae2b42d17be3bfbdac1808445..c3f3bd219b3d59bd7f7d989bc4ea47f46019bd68 100644
--- a/theories/proofmode/class_instances_bi.v
+++ b/theories/proofmode/class_instances_bi.v
@@ -730,7 +730,7 @@ Global Instance into_sep_and_persistent_l P P' Q Q' :
   Persistent P → AndIntoSep P P' Q Q' → IntoSep (P ∧ Q) P' Q'.
 Proof.
   destruct 2 as [P Q Q'|P Q]; rewrite /IntoSep.
-  - rewrite -(from_affinely Q') -(affine_affinely P) affinely_and_lr.
+  - rewrite -(from_affinely Q' Q) -(affine_affinely P) affinely_and_lr.
     by rewrite persistent_and_affinely_sep_l_1.
   - by rewrite persistent_and_affinely_sep_l_1.
 Qed.
@@ -738,7 +738,7 @@ Global Instance into_sep_and_persistent_r P P' Q Q' :
   Persistent Q → AndIntoSep Q Q' P P' → IntoSep (P ∧ Q) P' Q'.
 Proof.
   destruct 2 as [Q P P'|Q P]; rewrite /IntoSep.
-  - rewrite -(from_affinely P') -(affine_affinely Q) -affinely_and_lr.
+  - rewrite -(from_affinely P' P) -(affine_affinely Q) -affinely_and_lr.
     by rewrite persistent_and_affinely_sep_r_1.
   - by rewrite persistent_and_affinely_sep_r_1.
 Qed.
diff --git a/theories/proofmode/class_instances_sbi.v b/theories/proofmode/class_instances_sbi.v
index b23e54df1be72188c71d5f8c59d694cca4fd1736..2748471ca226eed336d9962b07fd66fb9cb46e02 100644
--- a/theories/proofmode/class_instances_sbi.v
+++ b/theories/proofmode/class_instances_sbi.v
@@ -392,7 +392,7 @@ Proof. by rewrite /FromModal. Qed.
 Global Instance from_modal_plainly_embed `{BiPlainly PROP, BiPlainly PROP',
     BiEmbedPlainly PROP PROP', !SbiEmbed PROP PROP'} `(sel : A) P Q :
   FromModal modality_plainly sel P Q →
-  FromModal modality_plainly sel ⎡P⎤ ⎡Q⎤ | 100.
+  FromModal (PROP2:=PROP') modality_plainly sel ⎡P⎤ ⎡Q⎤ | 100.
 Proof. rewrite /FromModal /= =><-. by rewrite embed_plainly. Qed.
 
 (** IntoInternalEq *)
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 310bcaabdf9c9f4053268690c0878fe7f7f33cba..abd98b1a794ed2dc623698ddd05f37b56a5d93e1 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -285,7 +285,7 @@ Proof. done. Qed.
 
 Class Frame {PROP : bi} (p : bool) (R P Q : PROP) := frame : □?p R ∗ Q ⊢ P.
 Arguments Frame {_} _ _%I _%I _%I.
-Arguments frame {_ _} _%I _%I _%I {_}.
+Arguments frame {_} _ _%I _%I _%I {_}.
 Hint Mode Frame + + ! ! - : typeclass_instances.
 
 (* The boolean [progress] indicates whether actual framing has been performed.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 426f5263ce01d1bf4ba0b029518b1b1fb5bd54a4..6291971cbb22b43393cf2583023d8451f2eed9a7 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -109,7 +109,7 @@ Qed.
 Lemma tac_pure_intro Δ Q φ af :
   env_spatial_is_nil Δ = af → FromPure af Q φ → φ → envs_entails Δ Q.
 Proof.
-  intros ???. rewrite envs_entails_eq -(from_pure _ Q). destruct af.
+  intros ???. rewrite envs_entails_eq -(from_pure af Q). destruct af.
   - rewrite env_spatial_is_nil_intuitionistically //= /bi_intuitionistically.
     f_equiv. by apply pure_intro.
   - by apply pure_intro.
@@ -145,7 +145,7 @@ Lemma tac_intuitionistic Δ Δ' i p P P' Q :
 Proof.
   rewrite envs_entails_eq=>?? HPQ ? HQ. rewrite envs_replace_singleton_sound //=.
   destruct p; simpl; rewrite /bi_intuitionistically.
-  - by rewrite -(into_persistent _ P) /= wand_elim_r.
+  - by rewrite -(into_persistent true P) /= wand_elim_r.
   - destruct HPQ.
     + rewrite -(affine_affinely P) (_ : P = <pers>?false P)%I //
               (into_persistent _ P) wand_elim_r //.
@@ -165,10 +165,10 @@ Proof.
   rewrite /FromImpl envs_entails_eq => <- ??? <-. destruct (env_spatial_is_nil Δ) eqn:?.
   - rewrite (env_spatial_is_nil_intuitionistically Δ) //; simpl. apply impl_intro_l.
     rewrite envs_app_singleton_sound //; simpl.
-    rewrite -(from_affinely P') -affinely_and_lr.
+    rewrite -(from_affinely P' P) -affinely_and_lr.
     by rewrite persistently_and_intuitionistically_sep_r intuitionistically_elim wand_elim_r.
   - apply impl_intro_l. rewrite envs_app_singleton_sound //; simpl.
-    by rewrite -(from_affinely P') persistent_and_affinely_sep_l_1 wand_elim_r.
+    by rewrite -(from_affinely P' P) persistent_and_affinely_sep_l_1 wand_elim_r.
 Qed.
 Lemma tac_impl_intro_intuitionistic Δ Δ' i P P' Q R :
   FromImpl R P Q →
@@ -251,7 +251,7 @@ Proof.
     destruct (envs_app _ _ _) eqn:?; simplify_eq/=.
   rewrite envs_lookup_sound // envs_split_sound //.
   rewrite (envs_app_singleton_sound Δ2) //; simpl.
-  rewrite HP1 into_wand /= -(add_modal P1' P1 Q). cancel [P1'].
+  rewrite HP1 (into_wand q false) /= -(add_modal P1' P1 Q). cancel [P1'].
   apply wand_intro_l. by rewrite assoc !wand_elim_r.
 Qed.
 
@@ -272,7 +272,7 @@ Lemma tac_specialize_frame Δ Δ' j q R P1 P2 P1' Q Q' :
 Proof.
   rewrite envs_entails_eq. intros [? ->]%envs_lookup_delete_Some ?? HPQ ->.
   rewrite envs_lookup_sound //. rewrite HPQ -lock.
-  rewrite into_wand -{2}(add_modal P1' P1 Q). cancel [P1'].
+  rewrite (into_wand q false) -{2}(add_modal P1' P1 Q). cancel [P1'].
   apply wand_intro_l. by rewrite assoc !wand_elim_r.
 Qed.
 
@@ -284,7 +284,8 @@ Lemma tac_specialize_assert_pure Δ Δ' j q R P1 P2 φ Q :
   φ → envs_entails Δ' Q → envs_entails Δ Q.
 Proof.
   rewrite envs_entails_eq=> ????? <-. rewrite envs_simple_replace_singleton_sound //=.
-  rewrite -intuitionistically_if_idemp into_wand /= -(from_pure _ P1) /bi_intuitionistically.
+  rewrite -intuitionistically_if_idemp (into_wand q true) /=.
+  rewrite -(from_pure true P1) /bi_intuitionistically.
   rewrite pure_True //= persistently_affinely_elim persistently_pure
           affinely_True_emp affinely_emp.
   by rewrite emp_wand wand_elim_r.
@@ -302,11 +303,11 @@ Proof.
   rewrite envs_lookup_sound //.
   rewrite -(idemp bi_and (of_envs (envs_delete _ _ _ _))).
   rewrite {2}envs_simple_replace_singleton_sound' //; simpl.
-  rewrite {1}HP1 (into_absorbingly P1') (persistent_persistently_2 P1).
+  rewrite {1}HP1 (into_absorbingly P1' P1) (persistent_persistently_2 P1).
   rewrite absorbingly_elim_persistently persistently_and_intuitionistically_sep_l assoc.
   rewrite -intuitionistically_if_idemp -intuitionistically_idemp.
   rewrite (intuitionistically_intuitionistically_if q).
-  by rewrite intuitionistically_if_sep_2 into_wand wand_elim_l wand_elim_r.
+  by rewrite intuitionistically_if_sep_2 (into_wand q true) wand_elim_l wand_elim_r.
 Qed.
 
 Lemma tac_specialize_intuitionistic_helper Δ Δ'' j q P R R' Q :
@@ -402,7 +403,7 @@ Lemma tac_apply Δ Δ' i p R P1 P2 :
   envs_entails Δ' P1 → envs_entails Δ P2.
 Proof.
   rewrite envs_entails_eq => ?? HP1. rewrite envs_lookup_delete_sound //.
-  by rewrite into_wand /= HP1 wand_elim_l.
+  by rewrite (into_wand p false) /= HP1 wand_elim_l.
 Qed.
 
 (** * Conjunction splitting *)
@@ -487,7 +488,7 @@ Qed.
 Lemma tac_frame_pure Δ (φ : Prop) P Q :
   φ → Frame true ⌜φ⌝ P Q → envs_entails Δ Q → envs_entails Δ P.
 Proof.
-  rewrite envs_entails_eq => ?? ->. rewrite -(frame ⌜φ⌝ P) /=.
+  rewrite envs_entails_eq => ?? ->. rewrite -(frame true ⌜φ⌝ P) /=.
   rewrite -persistently_and_intuitionistically_sep_l persistently_pure.
   auto using and_intro, pure_intro.
 Qed.
@@ -498,7 +499,7 @@ Lemma tac_frame Δ Δ' i p R P Q :
   envs_entails Δ' Q → envs_entails Δ P.
 Proof.
   rewrite envs_entails_eq. intros [? ->]%envs_lookup_delete_Some ? HQ.
-  rewrite (envs_lookup_sound' _ false) //. by rewrite -(frame R P) HQ.
+  rewrite (envs_lookup_sound' _ false) //. by rewrite -(frame p R P) HQ.
 Qed.
 
 (** * Disjunction *)
diff --git a/theories/proofmode/frame_instances.v b/theories/proofmode/frame_instances.v
index 278bcbf90eada13840fdd961f9bc015bcb0341c0..63e837fcd785e3ced506b32d6d20cfc4ae50d5b8 100644
--- a/theories/proofmode/frame_instances.v
+++ b/theories/proofmode/frame_instances.v
@@ -33,10 +33,10 @@ Proof.
 Qed.
 
 Global Instance make_embed_pure `{BiEmbed PROP PROP'} φ :
-  KnownMakeEmbed ⌜φ⌝ ⌜φ⌝.
+  KnownMakeEmbed (PROP:=PROP) ⌜φ⌝ ⌜φ⌝.
 Proof. apply embed_pure. Qed.
 Global Instance make_embed_emp `{BiEmbedEmp PROP PROP'} :
-  KnownMakeEmbed emp emp.
+  KnownMakeEmbed (PROP:=PROP) emp emp.
 Proof. apply embed_emp. Qed.
 Global Instance make_embed_default `{BiEmbed PROP PROP'} P :
   MakeEmbed P ⎡P⎤ | 100.
@@ -296,14 +296,14 @@ Global Instance make_laterN_default P : MakeLaterN n P (â–·^n P) | 100.
 Proof. by rewrite /MakeLaterN. Qed.
 
 Global Instance frame_later p R R' P Q Q' :
-  NoBackTrack (MaybeIntoLaterN true 1 R' R) →
+  TCNoBackTrack (MaybeIntoLaterN true 1 R' R) →
   Frame p R P Q → MakeLaterN 1 Q Q' → Frame p R' (▷ P) Q'.
 Proof.
   rewrite /Frame /MakeLaterN /MaybeIntoLaterN=>-[->] <- <-.
   by rewrite later_intuitionistically_if_2 later_sep.
 Qed.
 Global Instance frame_laterN p n R R' P Q Q' :
-  NoBackTrack (MaybeIntoLaterN true n R' R) →
+  TCNoBackTrack (MaybeIntoLaterN true n R' R) →
   Frame p R P Q → MakeLaterN n Q Q' → Frame p R' (▷^n P) Q'.
 Proof.
   rewrite /Frame /MakeLaterN /MaybeIntoLaterN=>-[->] <- <-.
diff --git a/theories/proofmode/reduction.v b/theories/proofmode/reduction.v
index 0db1e202a4da65b2c6275ec641b4a69a9941ecf2..1c48602219c85f36c83c59c5e7ee171006e48321 100644
--- a/theories/proofmode/reduction.v
+++ b/theories/proofmode/reduction.v
@@ -20,7 +20,9 @@ Declare Reduction pm_eval := cbv [
 Ltac pm_eval t :=
   eval pm_eval in t.
 Ltac pm_reduce :=
-  match goal with |- ?u => let v := pm_eval u in change v end.
+  (* Use [convert_concl_no_check] instead of [change] to avoid performing the
+  conversion check twice. *)
+  match goal with |- ?u => let v := pm_eval u in convert_concl_no_check v end.
 Ltac pm_reflexivity := pm_reduce; exact eq_refl.
 
 (** Called by many tactics for redexes that are created by instantiation.
@@ -34,4 +36,6 @@ Declare Reduction pm_prettify := cbn [
   bi_tforall bi_texist
 ].
 Ltac pm_prettify :=
-  match goal with |- ?u => let v := eval pm_prettify in u in change v end.
+  (* Use [convert_concl_no_check] instead of [change] to avoid performing the
+  conversion check twice. *)
+  match goal with |- ?u => let v := eval pm_prettify in u in convert_concl_no_check v end.