diff --git a/opam b/opam
index 4c340587b0d956c13128b427a352b9f0e5daf9e1..373cfee4402dc9901ff93896488bd371a1f2b7b5 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-04-25.0.0f2d2c8a") | (= "dev") }
+  "coq-stdpp" { (= "dev.2019-04-25.1.d6eb24f2") | (= "dev") }
 ]
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index d4418c515e2d989ff513ce006dfa32448a8228e1..86b3c0c97e2e4d16de541fa879781a5c02798956 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.
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/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/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..19976c17d024be36ea123ef6540f85269c0c43c1 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.