diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 34d52265be0f8d05e97247815472e27f21d3c97b..9d4fe2027d05cd9e889c46bac5982279fc98b6db 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -98,8 +98,17 @@ The command has indeed failed with message:
 Tactic failure: iSpecialize: Q not persistent.
 "test_iAssert_intuitionistic"
      : string
-The command has indeed failed with message:
-Tactic failure: iSpecialize: (|==> P)%I not persistent.
+1 subgoal
+  
+  PROP : bi
+  BiBUpd0 : BiBUpd PROP
+  P : PROP
+  ============================
+  "HP" : P
+  "HPupd1" : |==> P
+  --------------------------------------â–¡
+  <pers> (|==> P)
+  
 The command has indeed failed with message:
 Tactic failure: iSpecialize: cannot instantiate (∀ _ : φ, P -∗ False)%I with
 P.
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 1c083285540092977af4c86c79c35e977f65bffc..0c3f43ab7d9fc06c4cf3fe908698614963495fdc 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -239,8 +239,10 @@ Proof.
   iIntros "#HP".
   (* Test that [HPupd1] ends up in the intuitionistic context *)
   iAssert (|==> P)%I with "[]" as "#HPupd1"; first done.
-  (* This should not work, [|==> P] is not persistent. *)
-  Fail iAssert (|==> P)%I with "[#]" as "#HPupd2"; first done.
+  (* Since [|==> P] is not persistent, this should create a goal with a <pers>
+  modality. *)
+  iAssert (|==> P)%I with "[#]" as "#HPupd2".
+  { Show. done. }
   done.
 Qed.
 
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 5159c0a588fb4c3cc6b1f517bd708063a669345c..f56763eb328bbb78f264cb0449cc4d9451f26a1d 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -393,21 +393,20 @@ Qed.
 Lemma tac_specialize_assert_intuitionistic Δ j q P1 P1' P2 R Q :
   envs_lookup j Δ = Some (q, R) →
   IntoWand q true R P1 P2 →
-  Persistent P1 →
-  IntoAbsorbingly P1' P1 →
+  MakePersistently P1 P1' →
   envs_entails (envs_delete true j q Δ) P1' →
   match envs_simple_replace j q (Esnoc Enil j P2) Δ with
   | Some Δ'' => envs_entails Δ'' Q
   | None => False
   end → envs_entails Δ Q.
 Proof.
-  rewrite envs_entails_eq => ???? HP1 HQ.
+  rewrite /MakePersistently envs_entails_eq => ?? HP HΔ HQ.
   destruct (envs_simple_replace _ _ _ _) as [Δ''|] eqn:?; last done.
   rewrite -HQ 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' P1) (persistent_persistently_2 P1).
-  rewrite absorbingly_elim_persistently persistently_and_intuitionistically_sep_l assoc.
+  rewrite {1}HΔ -HP.
+  rewrite 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 q true) wand_elim_l wand_elim_r.
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index aabad6df9cb8e5d9855c08c923165196043f1dba..dc19ffa40e66e9c51930c5166a59997b26641183 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -911,14 +911,11 @@ Ltac iSpecializePat_go H1 pats :=
          |pm_reduce;
           iSpecializePat_go H1 pats]
     | SGoal (SpecGoal GIntuitionistic false ?Hs_frame [] ?d) :: ?pats =>
-       notypeclasses refine (tac_specialize_assert_intuitionistic _ H1 _ _ _ _ _ _ _ _ _ _ _ _);
+       notypeclasses refine (tac_specialize_assert_intuitionistic _ H1 _ _ _ _ _ _ _ _ _ _ _);
          [pm_reflexivity ||
           let H1 := pretty_ident H1 in
           fail "iSpecialize:" H1 "not found"
          |solve_to_wand H1
-         |iSolveTC ||
-          let Q := match goal with |- Persistent ?Q => Q end in
-          fail "iSpecialize:" Q "not persistent"
          |iSolveTC
          |pm_reduce; iFrame Hs_frame; solve_done d (*goal*)
          |pm_reduce; iSpecializePat_go H1 pats]