diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index cd15455b1f5146f32958b521111b58b64f36e363..24d4ed43605c386bb5a2b69d6e0476c6fa984cc4 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -130,10 +130,12 @@ Infix "â‹…?" := opM (at level 50, left associativity) : C_scope.
 (** * Persistent elements *)
 Class Persistent {A : cmraT} (x : A) := persistent : pcore x ≡ Some x.
 Arguments persistent {_} _ {_}.
+Hint Mode Persistent + ! : typeclass_instances.
 
 (** * Exclusive elements (i.e., elements that cannot have a frame). *)
 Class Exclusive {A : cmraT} (x : A) := exclusive0_l y : ✓{0} (x ⋅ y) → False.
 Arguments exclusive0_l {_} _ {_} _ _.
+Hint Mode Exclusive + ! : typeclass_instances.
 
 (** * CMRAs whose core is total *)
 (** The function [core] may return a dummy when used on CMRAs without total
@@ -545,7 +547,7 @@ Section ucmra.
   Global Instance cmra_unit_total : CMRATotal A.
   Proof.
     intros x. destruct (cmra_pcore_mono' ∅ x ∅) as (cx&->&?);
-      eauto using ucmra_unit_least, (persistent ∅).
+      eauto using ucmra_unit_least, (persistent (∅:A)).
   Qed.
 End ucmra.
 Hint Immediate cmra_unit_total.
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 2a4694ad4290faf4de41d5137ee43cc0ffdbdf0d..5285f7ef2ac259d2ad2c943476000a078fd3651e 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -72,8 +72,10 @@ Hint Extern 1 (_ ≡{_}≡ _) => apply equiv_dist; assumption.
 (** Discrete OFEs and Timeless elements *)
 (* TODO: On paper, We called these "discrete elements". I think that makes
    more sense. *)
-Class Timeless `{Equiv A, Dist A} (x : A) := timeless y : x ≡{0}≡ y → x ≡ y.
-Arguments timeless {_ _ _} _ {_} _ _.
+Class Timeless {A : ofeT} (x : A) := timeless y : x ≡{0}≡ y → x ≡ y.
+Arguments timeless {_} _ {_} _ _.
+Hint Mode Timeless + ! : typeclass_instances.
+
 Class Discrete (A : ofeT) := discrete_timeless (x : A) :> Timeless x.
 
 (** OFEs with a completion *)
@@ -1029,12 +1031,13 @@ Section sigma.
 
   Global Instance sig_timeless (x : sig P) :
     Timeless (proj1_sig x) → Timeless x.
-  Proof. intros ? y. destruct x, y. unfold dist, sig_dist, equiv, sig_equiv. apply (timeless _). Qed.
-  Global Instance sig_discrete_cofe : Discrete A → Discrete sigC.
   Proof.
-    intros ? [??] [??]. rewrite /dist /equiv /ofe_dist /ofe_equiv /=.
-    rewrite /sig_dist /sig_equiv /=. apply discrete_timeless.
-  Qed.
+    intros ? [b ?]; destruct x as [a ?].
+    rewrite /dist /ofe_dist /= /sig_dist /equiv /ofe_equiv /= /sig_equiv /=.
+    apply (timeless _).
+   Qed.
+  Global Instance sig_discrete_cofe : Discrete A → Discrete sigC.
+  Proof. intros ??. apply _. Qed.
 End sigma.
 
 Arguments sigC {_} _.
diff --git a/theories/algebra/vector.v b/theories/algebra/vector.v
index e0094eed172d4fa9e9d74e35a0273d6943d5b57b..1ee6ef12d4adb8989b9fff01017e7cad58f8c654 100644
--- a/theories/algebra/vector.v
+++ b/theories/algebra/vector.v
@@ -12,10 +12,10 @@ Section ofe.
   Definition vec_ofe_mixin m : OfeMixin (vec A m).
   Proof.
     split.
-    - intros x y. apply (equiv_dist (A:=listC A)).
+    - intros v w. apply (equiv_dist (A:=listC A)).
     - unfold dist, vec_dist. split.
         by intros ?. by intros ??. by intros ?????; etrans.
-    - intros. by apply (dist_S (A:=listC A)).
+    - intros n v w. by apply (dist_S (A:=listC A)).
   Qed.
   Canonical Structure vecC m : ofeT := OfeT (vec A m) (vec_ofe_mixin m).
 
@@ -48,22 +48,21 @@ Section proper.
     Proper (dist n ==> eq ==> dist n) (@Vector.nth A m).
   Proof.
     intros v. induction v as [|x m v IH]; intros v'; inv_vec v'.
-    - intros _ x. inversion x.
-    - intros x' v' EQ i ? <-. inversion_clear EQ. inv_fin i; first done.
-      intros i. by apply IH.
+    - intros _ x. inv_fin x.
+    - intros x' v' EQ i ? <-. inversion_clear EQ. inv_fin i=> // i. by apply IH.
   Qed.
   Global Instance vlookup_proper m :
     Proper (equiv ==> eq ==> equiv) (@Vector.nth A m).
   Proof.
-    intros ??????. apply equiv_dist=>?. subst. f_equiv. by apply equiv_dist.
+    intros v v' ? x x' ->. apply equiv_dist=> n. f_equiv. by apply equiv_dist.
   Qed.
 
   Global Instance vec_to_list_ne n m :
     Proper (dist n ==> dist n) (@vec_to_list A m).
-  Proof. intros ?? H. apply H. Qed.
+  Proof. by intros v v'. Qed.
   Global Instance vec_to_list_proper m :
     Proper (equiv ==> equiv) (@vec_to_list A m).
-  Proof. intros ?? H. apply H. Qed.
+  Proof. by intros v v'. Qed.
 End proper.
 
 Section cofe.
@@ -95,7 +94,7 @@ Instance vec_map_ne {A B : ofeT} m f n :
   Proper (dist n ==> dist n) f →
   Proper (dist n ==> dist n) (@vec_map A B m f).
 Proof.
-  intros ??? H. eapply list_fmap_ne in H; last done.
+  intros ? v v' H. eapply list_fmap_ne in H; last done.
   by rewrite -!vec_to_list_map in H.
 Qed.
 Definition vecC_map {A B : ofeT} m (f : A -n> B) : vecC A m -n> vecC B m :=
diff --git a/theories/base_logic/big_op.v b/theories/base_logic/big_op.v
index 8644cfaba005bdfb16cdf35c071fe1deee7ece01..64075f8b7f5145187dc5263e8a25197a0c415835 100644
--- a/theories/base_logic/big_op.v
+++ b/theories/base_logic/big_op.v
@@ -115,10 +115,12 @@ Notation "'[∗' 'mset' ] x ∈ X , P" := (big_opMS (M:=uPredUR _) X (λ x, P))
 Class PersistentL {M} (Ps : list (uPred M)) :=
   persistentL : Forall PersistentP Ps.
 Arguments persistentL {_} _ {_}.
+Hint Mode PersistentL + ! : typeclass_instances.
 
 Class TimelessL {M} (Ps : list (uPred M)) :=
   timelessL : Forall TimelessP Ps.
 Arguments timelessL {_} _ {_}.
+Hint Mode TimelessP + ! : typeclass_instances.
 
 (** * Properties *)
 Section big_op.
diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index 679db07daf2433af296e6fd92e04d7485510425a..c812280a89ef8419a483d55caa9ebdcc45d729e4 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -31,10 +31,12 @@ Typeclasses Opaque uPred_except_0.
 
 Class TimelessP {M} (P : uPred M) := timelessP : ▷ P ⊢ ◇ P.
 Arguments timelessP {_} _ {_}.
+Hint Mode TimelessP + ! : typeclass_instances.
 
 Class PersistentP {M} (P : uPred M) := persistentP : P ⊢ □ P.
 Hint Mode PersistentP - ! : typeclass_instances.
 Arguments persistentP {_} _ {_}.
+Hint Mode PersistentP + ! : typeclass_instances.
 
 Module uPred.
 Section derived.
@@ -808,9 +810,43 @@ Global Instance from_option_timeless {A} P (Ψ : A → uPred M) (mx : option A)
   (∀ x, TimelessP (Ψ x)) → TimelessP P → TimelessP (from_option Ψ P mx).
 Proof. destruct mx; apply _. Qed.
 
+(* Derived lemmas for persistence *)
+Lemma always_always P `{!PersistentP P} : □ P ⊣⊢ P.
+Proof. apply (anti_symm (⊢)); auto using always_elim. Qed.
+Lemma always_if_always p P `{!PersistentP P} : □?p P ⊣⊢ P.
+Proof. destruct p; simpl; auto using always_always. Qed.
+Lemma always_intro P Q `{!PersistentP P} : (P ⊢ Q) → P ⊢ □ Q.
+Proof. rewrite -(always_always P); apply always_intro'. Qed.
+Lemma always_and_sep_l P Q `{!PersistentP P} : P ∧ Q ⊣⊢ P ∗ Q.
+Proof. by rewrite -(always_always P) always_and_sep_l'. Qed.
+Lemma always_and_sep_r P Q `{!PersistentP Q} : P ∧ Q ⊣⊢ P ∗ Q.
+Proof. by rewrite -(always_always Q) always_and_sep_r'. Qed.
+Lemma always_sep_dup P `{!PersistentP P} : P ⊣⊢ P ∗ P.
+Proof. by rewrite -(always_always P) -always_sep_dup'. Qed.
+Lemma always_entails_l P Q `{!PersistentP Q} : (P ⊢ Q) → P ⊢ Q ∗ P.
+Proof. by rewrite -(always_always Q); apply always_entails_l'. Qed.
+Lemma always_entails_r P Q `{!PersistentP Q} : (P ⊢ Q) → P ⊢ P ∗ Q.
+Proof. by rewrite -(always_always Q); apply always_entails_r'. Qed.
+Lemma always_impl_wand P `{!PersistentP P} Q : (P → Q) ⊣⊢ (P -∗ Q).
+Proof.
+  apply (anti_symm _); auto using impl_wand.
+  apply impl_intro_l. by rewrite always_and_sep_l wand_elim_r.
+Qed.
+
 (* Persistence *)
 Global Instance pure_persistent φ : PersistentP (⌜φ⌝ : uPred M)%I.
 Proof. by rewrite /PersistentP always_pure. Qed.
+Global Instance pure_impl_persistent φ Q :
+  PersistentP Q → PersistentP (⌜φ⌝ → Q)%I.
+Proof.
+  rewrite /PersistentP pure_impl_forall always_forall. auto using forall_mono.
+Qed.
+Global Instance pure_wand_persistent φ Q :
+  PersistentP Q → PersistentP (⌜φ⌝ -∗ Q)%I.
+Proof.
+  rewrite /PersistentP -always_impl_wand pure_impl_forall always_forall.
+  auto using forall_mono.
+Qed.
 Global Instance always_persistent P : PersistentP (â–¡ P).
 Proof. by intros; apply always_intro'. Qed.
 Global Instance and_persistent P Q :
@@ -843,23 +879,5 @@ Proof. intros. by rewrite /PersistentP always_ownM. Qed.
 Global Instance from_option_persistent {A} P (Ψ : A → uPred M) (mx : option A) :
   (∀ x, PersistentP (Ψ x)) → PersistentP P → PersistentP (from_option Ψ P mx).
 Proof. destruct mx; apply _. Qed.
-
-(* Derived lemmas for persistence *)
-Lemma always_always P `{!PersistentP P} : □ P ⊣⊢ P.
-Proof. apply (anti_symm (⊢)); auto using always_elim. Qed.
-Lemma always_if_always p P `{!PersistentP P} : □?p P ⊣⊢ P.
-Proof. destruct p; simpl; auto using always_always. Qed.
-Lemma always_intro P Q `{!PersistentP P} : (P ⊢ Q) → P ⊢ □ Q.
-Proof. rewrite -(always_always P); apply always_intro'. Qed.
-Lemma always_and_sep_l P Q `{!PersistentP P} : P ∧ Q ⊣⊢ P ∗ Q.
-Proof. by rewrite -(always_always P) always_and_sep_l'. Qed.
-Lemma always_and_sep_r P Q `{!PersistentP Q} : P ∧ Q ⊣⊢ P ∗ Q.
-Proof. by rewrite -(always_always Q) always_and_sep_r'. Qed.
-Lemma always_sep_dup P `{!PersistentP P} : P ⊣⊢ P ∗ P.
-Proof. by rewrite -(always_always P) -always_sep_dup'. Qed.
-Lemma always_entails_l P Q `{!PersistentP Q} : (P ⊢ Q) → P ⊢ Q ∗ P.
-Proof. by rewrite -(always_always Q); apply always_entails_l'. Qed.
-Lemma always_entails_r P Q `{!PersistentP Q} : (P ⊢ Q) → P ⊢ P ∗ Q.
-Proof. by rewrite -(always_always Q); apply always_entails_r'. Qed.
 End derived.
 End uPred.
diff --git a/theories/base_logic/lib/core.v b/theories/base_logic/lib/core.v
index 6630d803a2bc315e3fd795277883eda227559417..d070516b97f2ffe3f4a9a10e880d250b21fffbc6 100644
--- a/theories/base_logic/lib/core.v
+++ b/theories/base_logic/lib/core.v
@@ -8,7 +8,7 @@ Import uPred.
     in the shallow embedding. *)
 
 Definition coreP {M : ucmraT} (P : uPred M) : uPred M :=
-  (∀ `(!PersistentP Q, P ⊢ Q), Q)%I.
+  (∀ `(!PersistentP Q), ⌜P ⊢ Q⌝ → Q)%I.
 Instance: Params (@coreP) 1.
 Typeclasses Opaque coreP.
 
@@ -25,7 +25,7 @@ Section core.
   Global Instance coreP_mono : Proper ((⊢) ==> (⊢)) (@coreP M).
   Proof.
     rewrite /coreP. iIntros (P P' ?) "H"; iIntros (Q ??).
-    unshelve iApply ("H" $! Q). by etrans.
+    iApply ("H" $! Q with "[%]"). by etrans.
   Qed.
 
   Global Instance coreP_proper : Proper ((⊣⊢) ==> (⊣⊢)) (@coreP M).
diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v
index 91fe5efe52e871ac0852fad45daed0f803dfc238..13f572fe08f503855b7f2a08c4b87728b53d8169 100644
--- a/theories/base_logic/lib/fancy_updates.v
+++ b/theories/base_logic/lib/fancy_updates.v
@@ -155,8 +155,10 @@ Section proofmode_classes.
   Proof. rewrite /FromAssumption=>->. apply bupd_fupd. Qed.
 
   Global Instance into_wand_fupd E1 E2 R P Q :
-    IntoWand R P Q → IntoWand R (|={E1,E2}=> P) (|={E1,E2}=> Q) | 100.
-  Proof. rewrite /IntoWand=>->. apply wand_intro_l. by rewrite fupd_wand_r. Qed.
+    IntoWand R P Q → IntoWand' R (|={E1,E2}=> P) (|={E1,E2}=> Q) | 100.
+  Proof.
+    rewrite /IntoWand' /IntoWand=>->. apply wand_intro_l. by rewrite fupd_wand_r.
+  Qed.
 
   Global Instance from_sep_fupd E P Q1 Q2 :
     FromSep P Q1 Q2 → FromSep (|={E}=> P) (|={E}=> Q1) (|={E}=> Q2).
@@ -179,8 +181,8 @@ Section proofmode_classes.
   Global Instance is_except_0_fupd E1 E2 P : IsExcept0 (|={E1,E2}=> P).
   Proof. by rewrite /IsExcept0 except_0_fupd. Qed.
 
-  Global Instance into_modal_fupd E P : IntoModal P (|={E}=> P).
-  Proof. rewrite /IntoModal. apply fupd_intro. Qed.
+  Global Instance from_modal_fupd E P : FromModal (|={E}=> P) P.
+  Proof. rewrite /FromModal. apply fupd_intro. Qed.
 
   (* Put a lower priority compared to [elim_modal_fupd_fupd], so that
      it is not taken when the first parameter is not specified (in
diff --git a/theories/base_logic/lib/sts.v b/theories/base_logic/lib/sts.v
index ddedc7272a86ae7efd68e4ab18a0330bf7e23db7..ebfebfc343503af8c78625ac844b9f73c6b066d5 100644
--- a/theories/base_logic/lib/sts.v
+++ b/theories/base_logic/lib/sts.v
@@ -101,13 +101,13 @@ Section sts.
   Proof.
     iIntros "[Hinv Hγf]". rewrite /sts_ownS /sts_inv /sts_own.
     iDestruct "Hinv" as (s) "[>Hγ Hφ]".
-    iCombine "Hγ" "Hγf" as "Hγ"; iDestruct (own_valid with "Hγ") as %Hvalid.
+    iDestruct (own_valid_2 with "Hγ Hγf") as %Hvalid.
     assert (s ∈ S) by eauto using sts_auth_frag_valid_inv.
     assert (✓ sts_frag S T) as [??] by eauto using cmra_valid_op_r.
-    rewrite sts_op_auth_frag //.
     iModIntro; iExists s; iSplit; [done|]; iFrame "Hφ".
     iIntros (s' T') "[% Hφ]".
-    iMod (own_update with "Hγ") as "Hγ"; first eauto using sts_update_auth.
+    iMod (own_update_2 with "Hγ Hγf") as "Hγ".
+    { rewrite sts_op_auth_frag; [|done..]. by apply sts_update_auth. }
     iRevert "Hγ"; rewrite -sts_op_auth_frag_up; iIntros "[Hγ $]".
     iModIntro. iNext. iExists s'; by iFrame.
   Qed.
diff --git a/theories/prelude/vector.v b/theories/prelude/vector.v
index ca76406ed8201973f582fde7df28aa0c3357d89c..4cf8de8a55bf707885736d2451dfcbc89763ca7c 100644
--- a/theories/prelude/vector.v
+++ b/theories/prelude/vector.v
@@ -187,7 +187,8 @@ Proof.
 Defined.
 
 Ltac inv_vec v :=
-  match type of v with
+  let T := type of v in
+  match eval hnf in T with
   | vec _ 0 =>
     revert dependent v; match goal with |- ∀ v, @?P v => apply (vec_0_inv P) end
   | vec _ (S ?n) =>
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index b7477648a18b7d3ad8f7c8974db8a0a98a09a73c..54bab13e11fdd94aec4ad389bbf58d244137916c 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -219,15 +219,22 @@ Proof. apply and_elim_r', impl_wand. Qed.
 
 Global Instance into_wand_always R P Q : IntoWand R P Q → IntoWand (□ R) P Q.
 Proof. rewrite /IntoWand=> ->. apply always_elim. Qed.
+
 Global Instance into_wand_later (R1 R2 P Q : uPred M) :
-  IntoLaterN 1 R1 R2 → IntoWand R2 P Q → IntoWand R1 (▷ P) (▷ Q) | 99.
-Proof. rewrite /IntoLaterN /IntoWand=> -> ->. by rewrite -later_wand. Qed.
+  IntoLaterN 1 R1 R2 → IntoWand R2 P Q → IntoWand' R1 (▷ P) (▷ Q) | 99.
+Proof.
+  rewrite /IntoLaterN /IntoWand' /IntoWand=> -> ->. by rewrite -later_wand.
+Qed.
 Global Instance into_wand_laterN n (R1 R2 P Q : uPred M) :
-  IntoLaterN n R1 R2 → IntoWand R2 P Q → IntoWand R1 (▷^n P) (▷^n Q) | 100.
-Proof. rewrite /IntoLaterN /IntoWand=> -> ->. by rewrite -laterN_wand. Qed.
+  IntoLaterN n R1 R2 → IntoWand R2 P Q → IntoWand' R1 (▷^n P) (▷^n Q) | 100.
+Proof.
+  rewrite /IntoLaterN /IntoWand' /IntoWand=> -> ->. by rewrite -laterN_wand.
+Qed.
 Global Instance into_wand_bupd R P Q :
-  IntoWand R P Q → IntoWand R (|==> P) (|==> Q) | 98.
-Proof. rewrite /IntoWand=>->. apply wand_intro_l. by rewrite bupd_wand_r. Qed.
+  IntoWand R P Q → IntoWand' R (|==> P) (|==> Q) | 98.
+Proof.
+  rewrite /IntoWand' /IntoWand=> ->. apply wand_intro_l. by rewrite bupd_wand_r.
+Qed.
 
 (* FromAnd *)
 Global Instance from_and_and P1 P2 : FromAnd (P1 ∧ P2) P1 P2.
@@ -564,12 +571,12 @@ Global Instance into_exist_laterN {A} n P (Φ : A → uPred M) :
   IntoExist P Φ → Inhabited A → IntoExist (▷^n P) (λ a, ▷^n (Φ a))%I.
 Proof. rewrite /IntoExist=> HP ?. by rewrite HP laterN_exist. Qed.
 
-(* IntoModal *)
-Global Instance into_modal_later P : IntoModal P (â–· P).
+(* FromModal *)
+Global Instance from_modal_later P : FromModal (â–· P) P.
 Proof. apply later_intro. Qed.
-Global Instance into_modal_bupd P : IntoModal P (|==> P).
+Global Instance from_modal_bupd P : FromModal (|==> P) P.
 Proof. apply bupd_intro. Qed.
-Global Instance into_modal_except_0 P : IntoModal P (â—‡ P).
+Global Instance from_modal_except_0 P : FromModal (â—‡ P) P.
 Proof. apply except_0_intro. Qed.
 
 (* ElimModal *)
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 8e66e89919bc52ffa72f6f0f0153bc4b900ff38a..0175bcfa3098b6178a77264a6c5469f5b147abbe 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -2,77 +2,102 @@ From iris.base_logic Require Export base_logic.
 Set Default Proof Using "Type".
 Import uPred.
 
-Section classes.
-Context {M : ucmraT}.
-Implicit Types P Q : uPred M.
-
-Class FromAssumption (p : bool) (P Q : uPred M) := from_assumption : □?p P ⊢ Q.
-Global Arguments from_assumption _ _ _ {_}.
-
-Class IntoPure (P : uPred M) (φ : Prop) := into_pure : P ⊢ ⌜φ⌝.
-Global Arguments into_pure : clear implicits.
-
-Class FromPure (P : uPred M) (φ : Prop) := from_pure : ⌜φ⌝ ⊢ P.
-Global Arguments from_pure : clear implicits.
-
-Class IntoPersistentP (P Q : uPred M) := into_persistentP : P ⊢ □ Q.
-Global Arguments into_persistentP : clear implicits.
-
-Class IntoLaterN (n : nat) (P Q : uPred M) := into_laterN : P ⊢ ▷^n Q.
-Global Arguments into_laterN _ _ _ {_}.
-
-Class FromLaterN (n : nat) (P Q : uPred M) := from_laterN : ▷^n Q ⊢ P.
-Global Arguments from_laterN _ _ _ {_}.
-
-Class IntoWand (R P Q : uPred M) := into_wand : R ⊢ P -∗ Q.
-Global Arguments into_wand : clear implicits.
-
-Class FromAnd (P Q1 Q2 : uPred M) := from_and : Q1 ∧ Q2 ⊢ P.
-Global Arguments from_and : clear implicits.
-
-Class FromSep (P Q1 Q2 : uPred M) := from_sep : Q1 ∗ Q2 ⊢ P.
-Global Arguments from_sep : clear implicits.
-
-Class IntoAnd (p : bool) (P Q1 Q2 : uPred M) :=
+Class FromAssumption {M} (p : bool) (P Q : uPred M) :=
+  from_assumption : □?p P ⊢ Q.
+Arguments from_assumption {_} _ _ _ {_}.
+Hint Mode FromAssumption + + ! - : typeclass_instances.
+
+Class IntoPure {M} (P : uPred M) (φ : Prop) := into_pure : P ⊢ ⌜φ⌝.
+Arguments into_pure {_} _ _ {_}.
+Hint Mode IntoPure + ! - : typeclass_instances.
+
+Class FromPure {M} (P : uPred M) (φ : Prop) := from_pure : ⌜φ⌝ ⊢ P.
+Arguments from_pure {_} _ _ {_}.
+Hint Mode FromPure + ! - : typeclass_instances.
+
+Class IntoPersistentP {M} (P Q : uPred M) := into_persistentP : P ⊢ □ Q.
+Arguments into_persistentP {_} _ _ {_}.
+Hint Mode IntoPersistentP + ! - : typeclass_instances.
+
+Class IntoLaterN {M} (n : nat) (P Q : uPred M) := into_laterN : P ⊢ ▷^n Q.
+Arguments into_laterN {_} _ _ _ {_}.
+Hint Mode IntoLaterN + - ! - : typeclass_instances.
+
+Class FromLaterN {M} (n : nat) (P Q : uPred M) := from_laterN : ▷^n Q ⊢ P.
+Arguments from_laterN {_} _ _ _ {_}.
+Hint Mode FromLaterN + - ! - : typeclass_instances.
+
+Class IntoWand {M} (R P Q : uPred M) := into_wand : R ⊢ P -∗ Q.
+Arguments into_wand {_} _ _ _ {_}.
+Hint Mode IntoWand + ! - - : typeclass_instances.
+
+Class IntoWand' {M} (R P Q : uPred M) := into_wand' :> IntoWand R P Q.
+Arguments into_wand' {_} _ _ _ {_}.
+Hint Mode IntoWand' + ! ! - : typeclass_instances.
+Hint Mode IntoWand' + ! - ! : typeclass_instances.
+
+Class FromAnd {M} (P Q1 Q2 : uPred M) := from_and : Q1 ∧ Q2 ⊢ P.
+Arguments from_and {_} _ _ _ {_}.
+Hint Mode FromAnd + ! - - : typeclass_instances.
+
+Class FromSep {M} (P Q1 Q2 : uPred M) := from_sep : Q1 ∗ Q2 ⊢ P.
+Arguments from_sep {_} _ _ _ {_}.
+Hint Mode FromSep + ! - - : typeclass_instances.
+Hint Mode FromSep + - ! ! : typeclass_instances. (* For iCombine *)
+
+Class IntoAnd {M} (p : bool) (P Q1 Q2 : uPred M) :=
   into_and : P ⊢ if p then Q1 ∧ Q2 else Q1 ∗ Q2.
-Global Arguments into_and : clear implicits.
-
-Lemma mk_into_and_sep p P Q1 Q2 : (P ⊢ Q1 ∗ Q2) → IntoAnd p P Q1 Q2.
+Arguments into_and {_} _ _ _ _ {_}.
+Hint Mode IntoAnd + + ! - - : typeclass_instances.
+Lemma mk_into_and_sep {M} p (P Q1 Q2 : uPred M) :
+  (P ⊢ Q1 ∗ Q2) → IntoAnd p P Q1 Q2.
 Proof. rewrite /IntoAnd=>->. destruct p; auto using sep_and. Qed.
 
 Class FromOp {A : cmraT} (a b1 b2 : A) := from_op : b1 ⋅ b2 ≡ a.
-Global Arguments from_op {_} _ _ _ {_}.
+Arguments from_op {_} _ _ _ {_}.
+Hint Mode FromOp + ! - - : typeclass_instances.
+Hint Mode FromOp + - ! ! : typeclass_instances. (* For iCombine *)
 
 Class IntoOp {A : cmraT} (a b1 b2 : A) := into_op : a ≡ b1 ⋅ b2.
-Global Arguments into_op {_} _ _ _ {_}.
+Arguments into_op {_} _ _ _ {_}.
+(* No [Hint Mode] since we want to turn [?x] into [?x1 â‹… ?x2], for example
+when having [H : own ?x]. *)
 
-Class Frame (R P Q : uPred M) := frame : R ∗ Q ⊢ P.
-Global Arguments frame : clear implicits.
+Class Frame {M} (R P Q : uPred M) := frame : R ∗ Q ⊢ P.
+Arguments frame {_} _ _ _ {_}.
+Hint Mode Frame + ! ! - : typeclass_instances.
 
-Class FromOr (P Q1 Q2 : uPred M) := from_or : Q1 ∨ Q2 ⊢ P.
-Global Arguments from_or : clear implicits.
+Class FromOr {M} (P Q1 Q2 : uPred M) := from_or : Q1 ∨ Q2 ⊢ P.
+Arguments from_or {_} _ _ _ {_}.
+Hint Mode FromOr + ! - - : typeclass_instances.
 
-Class IntoOr P Q1 Q2 := into_or : P ⊢ Q1 ∨ Q2.
-Global Arguments into_or : clear implicits.
+Class IntoOr {M} (P Q1 Q2 : uPred M) := into_or : P ⊢ Q1 ∨ Q2.
+Arguments into_or {_} _ _ _ {_}.
+Hint Mode IntoOr + ! - - : typeclass_instances.
 
-Class FromExist {A} (P : uPred M) (Φ : A → uPred M) :=
+Class FromExist {M A} (P : uPred M) (Φ : A → uPred M) :=
   from_exist : (∃ x, Φ x) ⊢ P.
-Global Arguments from_exist {_} _ _ {_}.
+Arguments from_exist {_ _} _ _ {_}.
+Hint Mode FromExist + - ! - : typeclass_instances.
 
-Class IntoExist {A} (P : uPred M) (Φ : A → uPred M) :=
+Class IntoExist {M A} (P : uPred M) (Φ : A → uPred M) :=
   into_exist : P ⊢ ∃ x, Φ x.
-Global Arguments into_exist {_} _ _ {_}.
+Arguments into_exist {_ _} _ _ {_}.
+Hint Mode IntoExist + - ! - : typeclass_instances.
 
-Class IntoModal (P Q : uPred M) := into_modal : P ⊢ Q.
-Global Arguments into_modal : clear implicits.
+Class FromModal {M} (P Q : uPred M) := from_modal : Q ⊢ P.
+Arguments from_modal {_} _ _ {_}.
+Hint Mode FromModal + ! - : typeclass_instances.
 
-Class ElimModal (P P' : uPred M) (Q Q' : uPred M) :=
+Class ElimModal {M} (P P' : uPred M) (Q Q' : uPred M) :=
   elim_modal : P ∗ (P' -∗ Q') ⊢ Q.
-Global Arguments elim_modal _ _ _ _ {_}.
+Arguments elim_modal {_} _ _ _ _ {_}.
+Hint Mode ElimModal + ! - ! - : typeclass_instances.
+Hint Mode ElimModal + - ! - ! : typeclass_instances.
 
-Lemma elim_modal_dummy P Q : ElimModal P P Q Q.
+Lemma elim_modal_dummy {M} (P Q : uPred M) : ElimModal P P Q Q.
 Proof. by rewrite /ElimModal wand_elim_r. Qed.
 
-Class IsExcept0 (Q : uPred M) := is_except_0 : ◇ Q ⊢ Q.
-Global Arguments is_except_0 : clear implicits.
-End classes.
+Class IsExcept0 {M} (Q : uPred M) := is_except_0 : ◇ Q ⊢ Q.
+Arguments is_except_0 {_} _ {_}.
+Hint Mode IsExcept0 + ! : typeclass_instances.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 394c5d7c3d8d1b461b2831f7760a3f2a033168e3..b78dad5245e046f47c6eaebb83a4f4b7d02316b6 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -832,8 +832,8 @@ Proof.
 Qed.
 
 (** * Modalities *)
-Lemma tac_modal_intro Δ P Q : IntoModal Q P → (Δ ⊢ Q) → Δ ⊢ P.
-Proof. rewrite /IntoModal. by intros <- ->. Qed.
+Lemma tac_modal_intro Δ P Q : FromModal P Q → (Δ ⊢ Q) → Δ ⊢ P.
+Proof. rewrite /FromModal. by intros <- ->. Qed.
 
 Lemma tac_modal_elim Δ Δ' i p P' P Q Q' :
   envs_lookup i Δ = Some (p, P) →
@@ -845,3 +845,5 @@ Proof.
   rewrite right_id HΔ always_if_elim. by apply elim_modal.
 Qed.
 End tactics.
+
+Hint Mode ForallSpecialize + - - ! - : typeclass_instances.
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index a2ddcee2a2dbc4fc6a4ab3428d689d94f3e0e65e..af482f59e08f483248faeec14181824246130d6a 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -426,13 +426,14 @@ Tactic Notation "iApply" open_constr(lem) :=
     | ITrm ?t ?xs ?pat => constr:(ITrm t xs ("*" +:+ pat))
     | _ => constr:(ITrm lem hnil "*")
     end in
-  iPoseProofCore lem as false true (fun H => first
-    [iExact H
-    |eapply tac_apply with _ H _ _ _;
+  let rec go H := first
+    [eapply tac_apply with _ H _ _ _;
       [env_cbv; reflexivity
-      |let P := match goal with |- IntoWand ?P _ _ => P end in
-       apply _ || fail 1 "iApply: cannot apply" P
-      |lazy beta (* reduce betas created by instantiation *)]]).
+      |apply _
+      |lazy beta (* reduce betas created by instantiation *)]
+    |iSpecializePat H "[-]"; last go H] in
+  iPoseProofCore lem as false true (fun H =>
+    first [iExact H|go H|iTypeOf H (fun Q => fail 1 "iApply: cannot apply" Q)]).
 
 (** * Revert *)
 Local Tactic Notation "iForallRevert" ident(x) :=
@@ -642,7 +643,7 @@ Tactic Notation "iNext":= iNext _.
 Tactic Notation "iModIntro" :=
   iStartProof;
   eapply tac_modal_intro;
-    [let P := match goal with |- IntoModal _ ?P => P end in
+    [let P := match goal with |- FromModal ?P _ => P end in
      apply _ || fail "iModIntro:" P "not a modality"|].
 
 Tactic Notation "iModCore" constr(H) :=
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 147edd8e6b6572b91d061697bfe4dd9de6bac8e3..f8302508d70aec9fefcb30f7045fc9e7e0ecd195 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -116,3 +116,7 @@ Proof.
   iAssert True%I with "[HP]" as %_. { Fail iClear "HQ". by iClear "HP". }
   done.
 Qed.
+
+Lemma demo_11 (M : ucmraT) (P Q R : uPred M) :
+  (P -∗ Q -∗ True -∗ True -∗ R) -∗ P -∗ Q -∗ R.
+Proof. iIntros "H HP HQ". by iApply ("H" with "[HP]"). Qed.