diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index e202bc38259a2c857cf2c034028ebb9425b2b7ff..2d1b5a7f9a97b87ddae308ab24f8cb29dbceed60 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -140,13 +140,13 @@ Proof.
 Qed.
 
 (* IntoPersistentP *)
-Global Instance into_persistentP_always_trans P Q :
-  IntoPersistentP P Q → IntoPersistentP (□ P) Q | 0.
-Proof. rewrite /IntoPersistentP=> ->. by rewrite always_always. Qed.
-Global Instance into_persistentP_always P : IntoPersistentP (â–¡ P) P | 1.
+Global Instance into_persistentP_always_trans p P Q :
+  IntoPersistentP true P Q → IntoPersistentP p (□ P) Q | 0.
+Proof. rewrite /IntoPersistentP /==> ->. by rewrite always_if_always. Qed.
+Global Instance into_persistentP_always P : IntoPersistentP true P P | 1.
 Proof. done. Qed.
 Global Instance into_persistentP_persistent P :
-  PersistentP P → IntoPersistentP P P | 100.
+  PersistentP P → IntoPersistentP false P P | 100.
 Proof. done. Qed.
 
 (* IntoLater *)
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 63b5adff57a012cb10f04713156ebde65b48e20b..336689a5c040c9691d48a125d7e229d7a3647410 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -27,9 +27,10 @@ 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 IntoPersistentP {M} (p : bool) (P Q : uPred M) :=
+  into_persistentP : □?p P ⊢ □ Q.
+Arguments into_persistentP {_} _ _ _ {_}.
+Hint Mode IntoPersistentP + + ! - : typeclass_instances.
 
 (* The class [IntoLaterN] has only two instances:
 
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 71e728e6f9019a5db90fb669f57608c7d84a1ec3..821092226a318e953c1a97e217590cd01b35016a 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -482,12 +482,13 @@ Proof.
 Qed.
 
 Lemma tac_persistent Δ Δ' i p P P' Q :
-  envs_lookup i Δ = Some (p, P) → IntoPersistentP P P' →
+  envs_lookup i Δ = Some (p, P) →
+  IntoPersistentP p P P' →
   envs_replace i p true (Esnoc Enil i P') Δ = Some Δ' →
   (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
-  intros ??? <-. rewrite envs_replace_sound //; simpl.
-  by rewrite right_id (into_persistentP P) always_if_always wand_elim_r.
+  intros ? HP ? <-. rewrite envs_replace_sound //; simpl.
+  by rewrite right_id (into_persistentP _ P) wand_elim_r.
 Qed.
 
 (** * Implication and wand *)
@@ -503,12 +504,13 @@ Proof.
     by rewrite always_and_sep_l right_id wand_elim_r.
 Qed.
 Lemma tac_impl_intro_persistent Δ Δ' i P P' Q :
-  IntoPersistentP P P' →
+  IntoPersistentP false P P' →
   envs_app true (Esnoc Enil i P') Δ = Some Δ' →
   (Δ' ⊢ Q) → Δ ⊢ P → Q.
 Proof.
-  intros ?? HQ. rewrite envs_app_sound //; simpl. apply impl_intro_l.
-  by rewrite right_id {1}(into_persistentP P) always_and_sep_l wand_elim_r.
+  intros ?? HQ. rewrite envs_app_sound //=; simpl. apply impl_intro_l.
+  rewrite (_ : P = â–¡?false P) // (into_persistentP false P).
+  by rewrite right_id always_and_sep_l wand_elim_r.
 Qed.
 Lemma tac_pure_impl_intro Δ (φ ψ : Prop) :
   (φ → Δ ⊢ ⌜ψ⌝) → Δ ⊢ ⌜φ → ψ⌝.
@@ -526,7 +528,7 @@ Proof.
   intros ? HQ. rewrite envs_app_sound //; simpl. by rewrite right_id HQ.
 Qed.
 Lemma tac_wand_intro_persistent Δ Δ' i P P' Q :
-  IntoPersistentP P P' →
+  IntoPersistentP false P P' →
   envs_app true (Esnoc Enil i P') Δ = Some Δ' →
   (Δ' ⊢ Q) → Δ ⊢ P -∗ Q.
 Proof.
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 3ae23afbedf8397af9d13387cb2b8dfc0fa7dd08..0e2e17af520703019260ccc515f0cb903f6866c0 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -160,7 +160,7 @@ Local Tactic Notation "iPersistent" constr(H) :=
   eapply tac_persistent with _ H _ _ _; (* (i:=H) *)
     [env_reflexivity || fail "iPersistent:" H "not found"
     |apply _ ||
-     let Q := match goal with |- IntoPersistentP ?Q _ => Q end in
+     let Q := match goal with |- IntoPersistentP _ ?Q _ => Q end in
      fail "iPersistent:" Q "not persistent"
     |env_reflexivity|].
 
@@ -317,14 +317,14 @@ Local Tactic Notation "iIntro" "#" constr(H) :=
   [ (* (?P → _) *)
     eapply tac_impl_intro_persistent with _ H _; (* (i:=H) *)
       [apply _ || 
-       let P := match goal with |- IntoPersistentP ?P _ => P end in
+       let P := match goal with |- IntoPersistentP _ ?P _ => P end in
        fail 1 "iIntro: " P " not persistent"
       |env_reflexivity || fail 1 "iIntro:" H "not fresh"
       |]
   | (* (?P -∗ _) *)
     eapply tac_wand_intro_persistent with _ H _; (* (i:=H) *)
       [apply _ || 
-       let P := match goal with |- IntoPersistentP ?P _ => P end in
+       let P := match goal with |- IntoPersistentP _ ?P _ => P end in
        fail 1 "iIntro: " P " not persistent"
       |env_reflexivity || fail 1 "iIntro:" H "not fresh"
       |]
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 59d960c0c29e26091a1e01ccded83ab8c3dbb467..7d12d2e27b2d6b1ea644f5a36ea1a2e382c40b2c 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -8,9 +8,9 @@ Implicit Types P Q R : uPred M.
 
 Lemma demo_0 P Q : □ (P ∨ Q) -∗ (∀ x, ⌜x = 0⌝ ∨ ⌜x = 1⌝) → (Q ∨ P).
 Proof.
-  iIntros "#H #H2".
+  iIntros "###H #H2".
   (* should remove the disjunction "H" *)
-  iDestruct "H" as "[?|?]"; last by iLeft.
+  iDestruct "H" as "[#?|#?]"; last by iLeft.
   (* should keep the disjunction "H" because it is instantiated *)
   iDestruct ("H2" $! 10) as "[%|%]". done. done.
 Qed.