diff --git a/ProofMode.md b/ProofMode.md
index 59846cef5fe77688ae9fb15a7bda9dc511c72212..ae2233edfd6bb004cc9aeccc786a8834ed4d570b 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -32,6 +32,10 @@ Context management
 - `iRename "H1" into "H2"` : rename the hypothesis `H1` into `H2`.
 - `iSpecialize pm_trm` : instantiate universal quantifiers and eliminate
   implications/wands of a hypothesis `pm_trm`. See proof mode terms below.
+- `iSpecialize pm_trm as #` : instantiate universal quantifiers and eliminate
+  implications/wands of a hypothesis whose conclusion is persistent. In this
+  case, all hypotheses can be used for proving the premises, as well as for
+  the resulting goal.
 - `iPoseProof pm_trm as "H"` : put `pm_trm` into the context as a new hypothesis
   `H`.
 - `iAssert P with "spat" as "ipat"` : create a new goal with conclusion `P` and
@@ -60,12 +64,17 @@ Elimination of logical connectives
 ----------------------------------
 
 - `iExFalso` : Ex falso sequitur quod libet.
-- `iDestruct pm_trm as (x1 ... xn) "spat1 ... spatn"` : elimination of
-  existential quantifiers using Coq introduction patterns `x1 ... xn` and
-  elimination of object level connectives using the proof mode introduction
-  patterns `ipat1 ... ipatn`.
+- `iDestruct pm_trm as (x1 ... xn) "ipat"` : elimination of existential
+  quantifiers using Coq introduction patterns `x1 ... xn` and elimination of
+  object level connectives using the proof mode introduction pattern `ipat`.
+  In case all branches of `ipat` start with an `#` (moving the hypothesis to the
+  persistent context) or `%` (moving the hypothesis to the pure Coq context),
+  one can use all hypotheses for proving the premises of `pm_trm`, as well as
+  for proving the resulting goal.
 - `iDestruct pm_trm as %cpat` : elimination of a pure hypothesis using the Coq
-  introduction pattern `cpat`.
+  introduction pattern `cpat`. When using this tactic, all hypotheses can be
+  used for proving the premises of `pm_trm`, as well as for proving the
+  resulting goal.
 
 Separating logic specific tactics
 ---------------------------------
@@ -180,9 +189,9 @@ so called specification patterns to express this splitting:
 - `==>[H1 ... Hn]` : same as the above pattern, but can only be used if the goal
   is a primitive view shift, in which case the view shift will be kept in the
   goal of the premise too.
-- `[#]` : This pattern can be used when eliminating `P -★ Q` when either `P` or
-  `Q` is persistent. In this case, all hypotheses are available in the goal for
-  the premise as none will be consumed.
+- `[#]` : This pattern can be used when eliminating `P -★ Q` with `P`
+  persistent. Using this pattern, all hypotheses are available in the goal for
+  `P`, as well the remaining goal.
 - `[%]` : This pattern can be used when eliminating `P -★ Q` when `P` is pure.
   It will generate a Coq goal for `P` and does not consume any hypotheses.
 - `*` : instantiate all top-level universal quantifiers with meta variables.
diff --git a/heap_lang/lib/ticket_lock.v b/heap_lang/lib/ticket_lock.v
index 219a66abee76f1816e6374cb0a87a8e779bba171..d4994cd762b91c116fb7ff35a469ee55bfa672cb 100644
--- a/heap_lang/lib/ticket_lock.v
+++ b/heap_lang/lib/ticket_lock.v
@@ -166,7 +166,7 @@ Section proof.
         as %[[[[?|] ?] [=]%leibniz_equiv_iff] ?]%auth_valid_discrete. }
     iDestruct "Haown" as "[[Hγo' _]|?]".
     { iCombine "Hγo" "Hγo'" as "Hγo".
-      iDestruct (own_valid with "#Hγo") as %[[] ?]. }
+      iDestruct (own_valid with "Hγo") as %[[] ?]. }
     iCombine "Hauth" "Hγo" as "Hauth".
     iVs (own_update with "Hauth") as "Hauth".
     { rewrite pair_split_L. apply: (auth_update _ _ (Excl' (S o), _)). (* FIXME: apply is slow *)
diff --git a/program_logic/adequacy.v b/program_logic/adequacy.v
index b2480ac7ed9d2e702f47e0b82cc2640da20b790b..5569939f7e2b865bfcc8675ecc0276f5cb8f6a3f 100644
--- a/program_logic/adequacy.v
+++ b/program_logic/adequacy.v
@@ -134,7 +134,7 @@ Proof.
   rewrite pvs_eq in HI;
     iVs (HI with "HI [Hw HE]") as "> (_ & _ & H)"; first by iFrame.
   iDestruct "H" as (σ2') "[Hσf %]".
-  iDestruct (ownP_agree σ2 σ2' with "[#]") as %<-. by iFrame. eauto.
+  iDestruct (ownP_agree σ2 σ2' with "[-]") as %<-. by iFrame. eauto.
 Qed.
 End adequacy.
 
diff --git a/program_logic/auth.v b/program_logic/auth.v
index a56f54d5b2e6533e2b15122dc6cb32db4e925339..99231ad4b0cf0597d3aba06bb77d80627a66e656 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -98,7 +98,7 @@ Section auth.
   Proof.
     iIntros (?) "(#? & >Hγf)". rewrite /auth_ctx /auth_own.
     iInv N as (a') "[>Hγ Hφ]" "Hclose". iCombine "Hγ" "Hγf" as "Hγ".
-    iDestruct (own_valid with "#Hγ") as % [[af Ha'] ?]%auth_valid_discrete.
+    iDestruct (own_valid with "Hγ") as % [[af Ha'] ?]%auth_valid_discrete.
     simpl in Ha'; rewrite ->(left_id _ _) in Ha'; setoid_subst.
     iVsIntro. iExists af; iFrame "Hφ"; iSplit; first done.
     iIntros (b) "[% Hφ]".
diff --git a/program_logic/boxes.v b/program_logic/boxes.v
index 97a46c231fdb095347c590bfbef6efd07a22353e..29c34b6b8d517dfad1da31caee94b0bb39434cba 100644
--- a/program_logic/boxes.v
+++ b/program_logic/boxes.v
@@ -118,8 +118,7 @@ Proof.
   iDestruct (big_sepM_delete _ f _ false with "Hf")
     as "[[Hγ' #[HγΦ ?]] ?]"; first done.
   iDestruct (box_own_agree γ Q (Φ γ) with "[#]") as "HeqQ"; first by eauto.
-  iDestruct (box_own_auth_agree γ b false with "[#]")
-    as "%"; subst; first by iFrame.
+  iDestruct (box_own_auth_agree γ b false with "[-]") as %->; first by iFrame.
   iSplitL "Hγ"; last iSplit.
   - iExists false; eauto.
   - iNext. iRewrite "HeqP". iRewrite "HeqQ". by rewrite -big_sepM_delete.
@@ -153,8 +152,7 @@ Proof.
   iDestruct (big_sepM_later _ f with "Hf") as "Hf".
   iDestruct (big_sepM_delete _ f with "Hf")
     as "[[>Hγ' #[HγΦ Hinv']] ?]"; first done.
-  iDestruct (box_own_auth_agree γ b true with "[#]")
-    as %?; subst; first by iFrame.
+  iDestruct (box_own_auth_agree γ b true with "[-]") as %->; first by iFrame.
   iFrame "HQ".
   iVs (box_own_auth_update γ with "[Hγ Hγ']") as "[Hγ Hγ']"; first by iFrame.
   iVs ("Hclose" with "[Hγ]"); first (iNext; iExists false; by repeat iSplit).
@@ -189,8 +187,7 @@ Proof.
     iAlways; iIntros (γ b ?) "(Hγ' & #$ & #$)".
     assert (true = b) as <- by eauto.
     iInv N as (b) "(>Hγ & _ & HΦ)" "Hclose".
-    iDestruct (box_own_auth_agree γ b true with "[#]")
-      as "%"; subst; first by iFrame.
+    iDestruct (box_own_auth_agree γ b true with "[-]") as %->; first by iFrame.
     iVs (box_own_auth_update γ true true false with "[Hγ Hγ']")
       as "[Hγ $]"; first by iFrame.
     iVs ("Hclose" with "[Hγ]"); first (iNext; iExists false; iFrame; eauto).
diff --git a/program_logic/lifting.v b/program_logic/lifting.v
index 1dcd9a8b070e1170939df6d504072b4e0e9efd20..16ef16d2ab251d56e2c66554f9021767519c8542 100644
--- a/program_logic/lifting.v
+++ b/program_logic/lifting.v
@@ -20,7 +20,7 @@ Lemma wp_lift_step E Φ e1 :
 Proof.
   iIntros (?) "H". rewrite wp_unfold /wp_pre; iRight; iSplit; auto.
   iIntros (σ1) "Hσ". iVs "H" as (σ1') "(% & >Hσf & H)".
-  iDestruct (ownP_agree σ1 σ1' with "[#]") as %<-; first by iFrame.
+  iDestruct (ownP_agree σ1 σ1' with "[-]") as %<-; first by iFrame.
   iVsIntro; iSplit; [done|]; iNext; iIntros (e2 σ2 efs Hstep).
   iVs (ownP_update σ1 σ2 with "[-H]") as "[$ ?]"; first by iFrame.
   iApply "H"; eauto.
diff --git a/program_logic/ownership.v b/program_logic/ownership.v
index aa42399a2fbe6873124186e7564ef59ca25d4d8b..b6f3ad902b6bd9784c805b54cd0a4b0303f5ed82 100644
--- a/program_logic/ownership.v
+++ b/program_logic/ownership.v
@@ -89,7 +89,7 @@ Proof. rewrite /ownE -own_op own_valid. by iIntros (?%coPset_disj_valid_op). Qed
 Lemma ownE_op' E1 E2 : E1 ⊥ E2 ∧ ownE (E1 ∪ E2) ⊣⊢ ownE E1 ★ ownE E2.
 Proof.
   iSplit; [iIntros "[% ?]"; by iApply ownE_op|].
-  iIntros "HE". iDestruct (ownE_disjoint with "#HE") as %?.
+  iIntros "HE". iDestruct (ownE_disjoint with "HE") as %?.
   iSplit; first done. iApply ownE_op; by try iFrame.
 Qed.
 Lemma ownE_singleton_twice i : ownE {[i]} ★ ownE {[i]} ⊢ False.
@@ -104,7 +104,7 @@ Proof. rewrite /ownD -own_op own_valid. by iIntros (?%gset_disj_valid_op). Qed.
 Lemma ownD_op' E1 E2 : E1 ⊥ E2 ∧ ownD (E1 ∪ E2) ⊣⊢ ownD E1 ★ ownD E2.
 Proof.
   iSplit; [iIntros "[% ?]"; by iApply ownD_op|].
-  iIntros "HE". iDestruct (ownD_disjoint with "#HE") as %?.
+  iIntros "HE". iDestruct (ownD_disjoint with "HE") as %?.
   iSplit; first done. iApply ownD_op; by try iFrame.
 Qed.
 Lemma ownD_singleton_twice i : ownD {[i]} ★ ownD {[i]} ⊢ False.
@@ -132,19 +132,19 @@ Qed.
 Lemma ownI_open i P : wsat ★ ownI i P ★ ownE {[i]} ⊢ wsat ★ ▷ P ★ ownD {[i]}.
 Proof.
   rewrite /ownI. iIntros "(Hw & Hi & HiE)". iDestruct "Hw" as (I) "[? HI]".
-  iDestruct (invariant_lookup I i P with "[#]") as (Q) "[% #HPQ]"; [by iFrame|].
+  iDestruct (invariant_lookup I i P with "[-]") as (Q) "[% #HPQ]"; [by iFrame|].
   iDestruct (big_sepM_delete _ _ i with "HI") as "[[[HQ $]|?] HI]"; eauto.
   - iSplitR "HQ"; last by iNext; iRewrite -"HPQ".
     iExists I. iFrame "Hw". iApply (big_sepM_delete _ _ i); eauto.
     iFrame "HI"; eauto.
-  - iDestruct (ownE_singleton_twice with "[#]") as %[]. by iFrame.
+  - iDestruct (ownE_singleton_twice with "[-]") as %[]. by iFrame.
 Qed.
 Lemma ownI_close i P : wsat ★ ownI i P ★ ▷ P ★ ownD {[i]} ⊢ wsat ★ ownE {[i]}.
 Proof.
   rewrite /ownI. iIntros "(Hw & Hi & HP & HiD)". iDestruct "Hw" as (I) "[? HI]".
-  iDestruct (invariant_lookup with "[#]") as (Q) "[% #HPQ]"; first by iFrame.
+  iDestruct (invariant_lookup with "[-]") as (Q) "[% #HPQ]"; first by iFrame.
   iDestruct (big_sepM_delete _ _ i with "HI") as "[[[HQ ?]|$] HI]"; eauto.
-  - iDestruct (ownD_singleton_twice with "[#]") as %[]. by iFrame.
+  - iDestruct (ownD_singleton_twice with "[-]") as %[]. by iFrame.
   - iExists I. iFrame "Hw". iApply (big_sepM_delete _ _ i); eauto.
     iFrame "HI". iLeft. iFrame "HiD". by iNext; iRewrite "HPQ".
 Qed.
diff --git a/program_logic/sts.v b/program_logic/sts.v
index 4693dc29d71f4f8da0476dcbdff5c6f20e6081bd..a27c28ce626975b1f37f8fa5642ef1b9c4a85445 100644
--- a/program_logic/sts.v
+++ b/program_logic/sts.v
@@ -95,7 +95,7 @@ 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.
+    iCombine "Hγ" "Hγf" as "Hγ"; iDestruct (own_valid with "Hγ") 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 //.
diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v
index 0d116ac97199e239e0466e730b17191de8e793a0..0917c2769e0a226e24ef15b77f57714312f8d3ab 100644
--- a/proofmode/coq_tactics.v
+++ b/proofmode/coq_tactics.v
@@ -488,7 +488,7 @@ Proof.
   by rewrite always_if_elim assoc !wand_elim_r.
 Qed.
 
-Lemma tac_specialize_pure Δ Δ' j q R P1 P2 φ Q :
+Lemma tac_specialize_assert_pure Δ Δ' j q R P1 P2 φ Q :
   envs_lookup j Δ = Some (q, R) →
   IntoWand R P1 P2 → FromPure P1 φ →
   envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ' →
@@ -498,24 +498,31 @@ Proof.
   by rewrite right_id (into_wand R) -(from_pure P1) // wand_True wand_elim_r.
 Qed.
 
-Lemma tac_specialize_persistent Δ Δ' Δ'' j q P1 P2 R Q :
+Lemma tac_specialize_assert_persistent Δ Δ' Δ'' j q P1 P2 R Q :
   envs_lookup_delete j Δ = Some (q, R, Δ') →
-  IntoWand R P1 P2 →
+  IntoWand R P1 P2 → PersistentP P1 →
   envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ'' →
-  (Δ' ⊢ P1) → (PersistentP P1 ∨ PersistentP P2) →
-  (Δ'' ⊢ Q) → Δ ⊢ Q.
+  (Δ' ⊢ P1) → (Δ'' ⊢ Q) → Δ ⊢ Q.
+Proof.
+  intros [? ->]%envs_lookup_delete_Some ??? HP1 <-.
+  rewrite envs_lookup_sound //.
+  rewrite -(idemp uPred_and (envs_delete _ _ _)).
+  rewrite {1}HP1 (persistentP P1) always_and_sep_l assoc.
+  rewrite envs_simple_replace_sound' //; simpl.
+  rewrite right_id (into_wand R) (always_elim_if q) -always_if_sep wand_elim_l.
+  by rewrite wand_elim_r.
+Qed.
+
+Lemma tac_specialize_persistent_helper Δ Δ' j q P R Q :
+  envs_lookup j Δ = Some (q,P) →
+  (Δ ⊢ R) → PersistentP R →
+  envs_replace j q true (Esnoc Enil j R) Δ = Some Δ' →
+  (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
-  intros [? ->]%envs_lookup_delete_Some ?? HP1 [?|?] <-.
-  - rewrite envs_lookup_sound //.
-    rewrite -(idemp uPred_and (envs_delete _ _ _)).
-    rewrite {1}HP1 (persistentP P1) always_and_sep_l assoc.
-    rewrite envs_simple_replace_sound' //; simpl.
-    rewrite right_id (into_wand R) (always_elim_if q) -always_if_sep wand_elim_l.
-    by rewrite wand_elim_r.
-  - rewrite -(idemp uPred_and Δ) {1}envs_lookup_sound //; simpl; rewrite HP1.
-    rewrite envs_simple_replace_sound //; simpl.
-    rewrite (sep_elim_r _ (_ -★ _)) right_id (into_wand R) always_if_elim.
-    by rewrite wand_elim_l always_and_sep_l -{1}(always_if_always q P2) wand_elim_r.
+  intros ? HR ?? <-.
+  rewrite -(idemp uPred_and Δ) {1}HR always_and_sep_l.
+  rewrite envs_replace_sound //; simpl.
+  by rewrite right_id assoc (sep_elim_l R) always_always wand_elim_r.
 Qed.
 
 Lemma tac_revert Δ Δ' i p P Q :
diff --git a/proofmode/intro_patterns.v b/proofmode/intro_patterns.v
index ac49db83957e8c257589e6b1940a64d5773e6f60..f2feecb4417f6276a4754a3d77781b213b67d0fc 100644
--- a/proofmode/intro_patterns.v
+++ b/proofmode/intro_patterns.v
@@ -19,6 +19,15 @@ Inductive intro_pat :=
   | IAll : intro_pat
   | IClear : list (bool * string) → intro_pat. (* true = frame, false = clear *)
 
+Fixpoint intro_pat_persistent (p : intro_pat) :=
+  match p with
+  | IPureElim => true
+  | IAlwaysElim _ => true
+  | ILaterElim p => intro_pat_persistent p
+  | IList pps => forallb (forallb intro_pat_persistent) pps
+  | _ => false
+  end.
+
 Module intro_pat.
 Inductive token :=
   | TName : string → token
diff --git a/proofmode/spec_patterns.v b/proofmode/spec_patterns.v
index 03f6d40f97dbd8b10b6edb5d3c8f8009f4c67b25..d72706b2f9a4c9a8eb93decd5176250bf6d3b677 100644
--- a/proofmode/spec_patterns.v
+++ b/proofmode/spec_patterns.v
@@ -6,7 +6,7 @@ Inductive spec_pat :=
   | SGoal : spec_goal_kind → bool → list string → spec_pat
   | SGoalPersistent : spec_pat
   | SGoalPure : spec_pat
-  | SName : bool → string → spec_pat (* first arg = persistent *)
+  | SName : string → spec_pat
   | SForall : spec_pat.
 
 Module spec_pat.
@@ -44,13 +44,12 @@ Inductive state :=
 Fixpoint parse_go (ts : list token) (k : list spec_pat) : option (list spec_pat) :=
   match ts with
   | [] => Some (rev k)
-  | TName s :: ts => parse_go ts (SName false s :: k)
+  | TName s :: ts => parse_go ts (SName s :: k)
   | TBracketL :: TPersistent :: TBracketR :: ts => parse_go ts (SGoalPersistent :: k)
   | TBracketL :: TPure :: TBracketR :: ts => parse_go ts (SGoalPure :: k)
   | TBracketL :: ts => parse_goal ts GoalStd false [] k
   | TVs :: TBracketL :: ts => parse_goal ts GoalVs false [] k
   | TVs :: ts => parse_go ts (SGoal GoalVs true [] :: k)
-  | TPersistent :: TName s :: ts => parse_go ts (SName true s :: k)
   | TForall :: ts => parse_go ts (SForall :: k)
   | _ => None
   end
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 3db566b13d7826a9f01b40c78c1764159af5dd5a..382e488aeb006550b1a2ce9a051a65217daea921 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -152,7 +152,7 @@ Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
     lazymatch pats with
     | [] => idtac
     | SForall :: ?pats => try (iSpecializeArgs H1 (hcons _ _)); go H1 pats
-    | SName false ?H2 :: ?pats =>
+    | SName ?H2 :: ?pats =>
        eapply tac_specialize with _ _ H2 _ H1 _ _ _ _; (* (j:=H1) (i:=H2) *)
          [env_cbv; reflexivity || fail "iSpecialize:" H2 "not found"
          |env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
@@ -160,30 +160,17 @@ Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
           let Q := match goal with |- IntoWand ?P ?Q _ => Q end in
           apply _ || fail "iSpecialize: cannot instantiate" P "with" Q
          |env_cbv; reflexivity|go H1 pats]
-    | SName true ?H2 :: ?pats =>
-       eapply tac_specialize_persistent with _ _ H1 _ _ _ _;
-         [env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
-         |solve_to_wand H1
-         |env_cbv; reflexivity
-         |iExact H2 || fail "iSpecialize:" H2 "not found or wrong type"
-         |let Q1 := match goal with |- PersistentP ?Q1 ∨ _ => Q1 end in
-          let Q2 := match goal with |- _ ∨ PersistentP ?Q2 => Q2 end in
-          first [left; apply _ | right; apply _]
-            || fail "iSpecialize:" Q1 "nor" Q2 "persistent"
-         |go H1 pats]
     | SGoalPersistent :: ?pats =>
-       eapply tac_specialize_persistent with _ _ H1 _ _ _ _;
+       eapply tac_specialize_assert_persistent with _ _ H1 _ _ _ _;
          [env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
          |solve_to_wand H1
+         |let Q := match goal with |- PersistentP ?Q => Q end in
+          apply _ || fail "iSpecialize:" Q "not persistent"
          |env_cbv; reflexivity
          |(*goal*)
-         |let Q1 := match goal with |- PersistentP ?Q1 ∨ _ => Q1 end in
-          let Q2 := match goal with |- _ ∨ PersistentP ?Q2 => Q2 end in
-          first [left; apply _ | right; apply _]
-            || fail "iSpecialize:" Q1 "nor" Q2 "persistent"
          |go H1 pats]
     | SGoalPure :: ?pats =>
-       eapply tac_specialize_pure with _ H1 _ _ _ _ _;
+       eapply tac_specialize_assert_pure with _ H1 _ _ _ _ _;
          [env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
          |solve_to_wand H1
          |let Q := match goal with |- FromPure ?Q _ => Q end in
@@ -204,11 +191,37 @@ Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
          |go H1 pats]
     end in let pats := spec_pat.parse pat in go H pats.
 
-Tactic Notation "iSpecialize" open_constr(t) :=
-  match t with
-  | ITrm ?H ?xs ?pat => iSpecializeArgs H xs; iSpecializePat H pat
+(* p = whether the conclusion of the specialized term is persistent. It can
+either be a Boolean or an introduction pattern, which will be coerced in true
+when it only contains `#` or `%` patterns at the top-level. *)
+Tactic Notation "iSpecializeCore" open_constr(t) "as" constr(p) tactic(tac) :=
+  let p :=
+    lazymatch type of p with
+    | intro_pat => eval cbv in (intro_pat_persistent p)
+    | string =>
+       let pat := intro_pat.parse_one p in
+       eval cbv in (intro_pat_persistent pat)
+    | _ => p
+    end in
+  lazymatch t with
+  | ITrm ?H ?xs ?pat =>
+    lazymatch p with
+    | true =>
+       eapply tac_specialize_persistent_helper with _ H _ _ _;
+         [env_cbv; reflexivity || fail "iSpecialize:" H "not found"
+         |iSpecializeArgs H xs; iSpecializePat H pat; last (iExact H)
+         |let Q := match goal with |- PersistentP ?Q => Q end in
+          apply _ || fail "iSpecialize:" Q "not persistent"
+         |env_cbv; reflexivity|tac H]
+    | false => iSpecializeArgs H xs; iSpecializePat H pat; last (tac H)
+    end
   end.
 
+Tactic Notation "iSpecialize" open_constr(t) :=
+  iSpecializeCore t as false (fun _ => idtac).
+Tactic Notation "iSpecialize" open_constr(t) "#" :=
+  iSpecializeCore t as true (fun _ => idtac).
+
 (** * Pose proof *)
 (* The tactic [iIntoEntails] tactic solves a goal [True ⊢ Q]. The arguments [t]
 is a Coq term whose type is of the following shape:
@@ -236,7 +249,7 @@ Tactic Notation "iIntoEntails" open_constr(t) :=
     end
   in go t.
 
-Tactic Notation "iPoseProofCore" open_constr(lem) "as" tactic(tac) :=
+Tactic Notation "iPoseProofCore" open_constr(lem) "as" constr(p) tactic(tac) :=
   let pose_trm t tac :=
     let Htmp := iFresh in
     lazymatch type of t with
@@ -255,16 +268,12 @@ Tactic Notation "iPoseProofCore" open_constr(lem) "as" tactic(tac) :=
     after the continuation [tac] has been called. *)
   in lazymatch lem with
   | ITrm ?t ?xs ?pat =>
-     pose_trm t ltac:(fun Htmp =>
-       iSpecializeArgs Htmp xs; iSpecializePat Htmp pat; last (tac Htmp))
+     pose_trm t ltac:(fun Htmp => iSpecializeCore (ITrm Htmp xs pat) as p tac)
   | _ => pose_trm lem tac
   end.
 
 Tactic Notation "iPoseProof" open_constr(lem) "as" constr(H) :=
-  iPoseProofCore lem as (fun Htmp => iRename Htmp into H).
-
-Tactic Notation "iPoseProof" open_constr(lem) :=
-  iPoseProofCore lem as (fun _ => idtac).
+  iPoseProofCore lem as false (fun Htmp => iRename Htmp into H).
 
 (** * Apply *)
 Tactic Notation "iApply" open_constr(lem) :=
@@ -277,12 +286,12 @@ Tactic Notation "iApply" open_constr(lem) :=
        |lazy beta (* reduce betas created by instantiation *)]] in
   lazymatch lem with
   | ITrm ?t ?xs ?pat =>
-     iPoseProofCore t as (fun Htmp =>
+     iPoseProofCore t as false (fun Htmp =>
        iSpecializeArgs Htmp xs;
        try (iSpecializeArgs Htmp (hcons _ _));
        iSpecializePat Htmp pat; last finish Htmp)
   | _ =>
-     iPoseProofCore lem as (fun Htmp =>
+     iPoseProofCore lem as false (fun Htmp =>
        try (iSpecializeArgs Htmp (hcons _ _));
        finish Htmp)
   end.
@@ -723,7 +732,7 @@ Tactic Notation "iIntros" "(" simple_intropattern(x1) simple_intropattern(x2)
   iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 ); iIntros p.
 
 (** * Destruct tactic *)
-Tactic Notation "iDestructCore" open_constr(lem) "as" tactic(tac) :=
+Tactic Notation "iDestructCore" open_constr(lem) "as" constr(p) tactic(tac) :=
   let intro_destruct n :=
     let rec go n' :=
       lazymatch n' with
@@ -738,49 +747,50 @@ Tactic Notation "iDestructCore" open_constr(lem) "as" tactic(tac) :=
      let n := eval compute in (Z.to_nat lem) in intro_destruct n
   | string => tac lem
   | iTrm =>
+     (* only copy the hypothesis when universal quantifiers are instantiated *)
      lazymatch lem with
-     | @iTrm string ?H _ hnil ?pat => iSpecializePat H pat; last (tac H)
-     | _ => iPoseProofCore lem as tac
+     | @iTrm string ?H _ hnil ?pat => iSpecializeCore lem as p tac
+     | _ => iPoseProofCore lem as p tac
      end
-  | _ => iPoseProofCore lem as tac
+  | _ => iPoseProofCore lem as p tac
   end.
 
 Tactic Notation "iDestruct" open_constr(lem) "as" constr(pat) :=
-  iDestructCore lem as (fun H => iDestructHyp H as pat).
+  iDestructCore lem as pat (fun H => iDestructHyp H as pat).
 Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1) ")"
     constr(pat) :=
-  iDestructCore lem as (fun H => iDestructHyp H as ( x1 ) pat).
+  iDestructCore lem as pat (fun H => iDestructHyp H as ( x1 ) pat).
 Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) ")" constr(pat) :=
-  iDestructCore lem as (fun H => iDestructHyp H as ( x1 x2 ) pat).
+  iDestructCore lem as pat (fun H => iDestructHyp H as ( x1 x2 ) pat).
 Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) ")" constr(pat) :=
-  iDestructCore lem as (fun H => iDestructHyp H as ( x1 x2 x3 ) pat).
+  iDestructCore lem as pat (fun H => iDestructHyp H as ( x1 x2 x3 ) pat).
 Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
     constr(pat) :=
-  iDestructCore lem as (fun H => iDestructHyp H as ( x1 x2 x3 x4 ) pat).
+  iDestructCore lem as pat (fun H => iDestructHyp H as ( x1 x2 x3 x4 ) pat).
 Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
     simple_intropattern(x5) ")" constr(pat) :=
-  iDestructCore lem as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 ) pat).
+  iDestructCore lem as pat (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 ) pat).
 Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
     simple_intropattern(x5) simple_intropattern(x6) ")" constr(pat) :=
-  iDestructCore lem as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 ) pat).
+  iDestructCore lem as pat (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 ) pat).
 Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
     simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) ")"
     constr(pat) :=
-  iDestructCore lem as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 ) pat).
+  iDestructCore lem as pat (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 ) pat).
 Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
     simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
     simple_intropattern(x8) ")" constr(pat) :=
-  iDestructCore lem as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat).
+  iDestructCore lem as pat (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat).
 
 Tactic Notation "iDestruct" open_constr(lem) "as" "%" simple_intropattern(pat) :=
-  iDestructCore lem as (fun H => iPure H as pat).
+  iDestructCore lem as true (fun H => iPure H as pat).
 
 (* This is pretty ugly, but without Ltac support for manipulating lists of
 idents I do not know how to do this better. *)
@@ -857,7 +867,7 @@ Local Ltac iRewriteFindPred :=
   end.
 
 Local Tactic Notation "iRewriteCore" constr(lr) open_constr(lem) :=
-  iPoseProofCore lem as (fun Heq =>
+  iPoseProofCore lem as true (fun Heq =>
     eapply (tac_rewrite _ Heq _ _ lr);
       [env_cbv; reflexivity || fail "iRewrite:" Heq "not found"
       |let P := match goal with |- ?P ⊢ _ => P end in
@@ -869,7 +879,7 @@ Tactic Notation "iRewrite" open_constr(lem) := iRewriteCore false lem.
 Tactic Notation "iRewrite" "-" open_constr(lem) := iRewriteCore true lem.
 
 Local Tactic Notation "iRewriteCore" constr(lr) open_constr(lem) "in" constr(H) :=
-  iPoseProofCore lem as (fun Heq =>
+  iPoseProofCore lem as true (fun Heq =>
     eapply (tac_rewrite_in _ Heq _ _ H _ _ lr);
       [env_cbv; reflexivity || fail "iRewrite:" Heq "not found"
       |env_cbv; reflexivity || fail "iRewrite:" H "not found"
@@ -890,45 +900,45 @@ Ltac iSimplifyEq := repeat (
 
 (** * View shifts *)
 Tactic Notation "iVs" open_constr(lem) :=
-  iDestructCore lem as (fun H => iVsCore H; last iDestruct H as "?").
+  iDestructCore lem as false (fun H => iVsCore H).
 Tactic Notation "iVs" open_constr(lem) "as" constr(pat) :=
-  iDestructCore lem as (fun H => iVsCore H; last iDestruct H as pat).
+  iDestructCore lem as false (fun H => iVsCore H; last iDestructHyp H as pat).
 Tactic Notation "iVs" open_constr(lem) "as" "(" simple_intropattern(x1) ")"
     constr(pat) :=
-  iDestructCore lem as (fun H => iVsCore H; last iDestruct H as ( x1 ) pat).
+  iDestructCore lem as false (fun H => iVsCore H; last iDestructHyp H as ( x1 ) pat).
 Tactic Notation "iVs" open_constr(lem) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) ")" constr(pat) :=
-  iDestructCore lem as (fun H => iVsCore H; last iDestruct H as ( x1 x2 ) pat).
+  iDestructCore lem as false (fun H => iVsCore H; last iDestructHyp H as ( x1 x2 ) pat).
 Tactic Notation "iVs" open_constr(lem) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) ")" constr(pat) :=
-  iDestructCore lem as (fun H => iVsCore H; last iDestruct H as ( x1 x2 x3 ) pat).
+  iDestructCore lem as false (fun H => iVsCore H; last iDestructHyp H as ( x1 x2 x3 ) pat).
 Tactic Notation "iVs" open_constr(lem) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
     constr(pat) :=
-  iDestructCore lem as (fun H =>
-    iVsCore H; last iDestruct H as ( x1 x2 x3 x4 ) pat).
+  iDestructCore lem as false (fun H =>
+    iVsCore H; last iDestructHyp H as ( x1 x2 x3 x4 ) pat).
 Tactic Notation "iVs" open_constr(lem) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
     simple_intropattern(x5) ")" constr(pat) :=
-  iDestructCore lem as (fun H =>
-    iVsCore H; last iDestruct H as ( x1 x2 x3 x4 x5 ) pat).
+  iDestructCore lem as false (fun H =>
+    iVsCore H; last iDestructHyp H as ( x1 x2 x3 x4 x5 ) pat).
 Tactic Notation "iVs" open_constr(lem) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
     simple_intropattern(x5) simple_intropattern(x6) ")" constr(pat) :=
-  iDestructCore lem as (fun H =>
-    iVsCore H; last iDestruct H as ( x1 x2 x3 x4 x5 x6 ) pat).
+  iDestructCore lem as false (fun H =>
+    iVsCore H; last iDestructHyp H as ( x1 x2 x3 x4 x5 x6 ) pat).
 Tactic Notation "iVs" open_constr(lem) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
     simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) ")"
     constr(pat) :=
-  iDestructCore lem as (fun H =>
-    iVsCore H; last iDestruct H as ( x1 x2 x3 x4 x5 x6 x7 ) pat).
+  iDestructCore lem as false (fun H =>
+    iVsCore H; last iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 ) pat).
 Tactic Notation "iVs" open_constr(lem) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
     simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
     simple_intropattern(x8) ")" constr(pat) :=
-  iDestructCore lem as (fun H =>
-    iVsCore H; last iDestruct H as ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat).
+  iDestructCore lem as false (fun H =>
+    iVsCore H; last iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat).
 
 (* Make sure that by and done solve trivial things in proof mode *)
 Hint Extern 0 (of_envs _ ⊢ _) => by iPureIntro.
diff --git a/tests/counter.v b/tests/counter.v
index c5e84d11d76f6f8bcbcd1098e63bc885a3fa5825..8d5bb62c1b5b1fe3a1cfb6497a8d3c26de647bf9 100644
--- a/tests/counter.v
+++ b/tests/counter.v
@@ -113,7 +113,7 @@ Proof.
   wp_bind (CAS _ _ _). iInv N as (c') ">[Hl Hγ]" "Hclose".
   destruct (decide (c' = c)) as [->|].
   - iCombine "Hγ" "Hγf" as "Hγ".
-    iDestruct (own_valid with "#Hγ") as %?%auth_frag_valid; rewrite -auth_frag_op //.
+    iDestruct (own_valid with "Hγ") as %?%auth_frag_valid; rewrite -auth_frag_op //.
     iVs (own_update with "Hγ") as "Hγ"; first apply M_update.
     rewrite (auth_frag_op (S n) (S c)); last lia; iDestruct "Hγ" as "[Hγ Hγf]".
     wp_cas_suc. iVs ("Hclose" with "[Hl Hγ]").
@@ -129,7 +129,7 @@ Lemma read_spec l n :
 Proof.
   iIntros "!# Hl /=". iDestruct "Hl" as (N γ) "(% & #Hh & #Hinv & Hγf)".
   rewrite /read /=. wp_let. iInv N as (c) "[Hl Hγ]" "Hclose". wp_load.
-  iDestruct (own_valid γ (Frag n ⋅ Auth c) with "[#]") as % ?%auth_frag_valid.
+  iDestruct (own_valid γ (Frag n ⋅ Auth c) with "[-]") as % ?%auth_frag_valid.
   { iApply own_op. by iFrame. }
   rewrite (auth_frag_op c c); last lia; iDestruct "Hγ" as "[Hγ Hγf']".
   iVs ("Hclose" with "[Hl Hγ]"); [iNext; iExists c; by iFrame|].
diff --git a/tests/joining_existentials.v b/tests/joining_existentials.v
index e06e47214277a05745f7981127303fd4ba54828a..78adb9719af808df78da53ccabbe052c2db0b042 100644
--- a/tests/joining_existentials.v
+++ b/tests/joining_existentials.v
@@ -95,6 +95,6 @@ Proof.
     + iApply worker_spec; auto.
     + iApply worker_spec; auto.
     + auto.
-  - iIntros (_ v) "[_ H]"; iPoseProof (Q_res_join with "H"). auto.
+  - iIntros (_ v) "[_ H]". iDestruct (Q_res_join with "H") as "?". auto.
 Qed.
 End proof.
diff --git a/tests/one_shot.v b/tests/one_shot.v
index 3e610b65d9ad5dd6d1549dc8575c201d0b16df37..92598f56215fafe323dfe9a0dd1e933d9f5d0aec 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -77,7 +77,7 @@ Proof.
     { iCombine "Hγ" "Hγ'" as "Hγ". by iDestruct (own_valid with "Hγ") as %?. }
     wp_load.
     iCombine "Hγ" "Hγ'" as "Hγ".
-    iDestruct (own_valid with "#Hγ") as %[=->]%dec_agree_op_inv.
+    iDestruct (own_valid with "Hγ") as %[=->]%dec_agree_op_inv.
     iVs ("Hclose" with "[Hl]") as "_".
     { iNext; iRight; by eauto. }
     iVsIntro. wp_match. iApply wp_assert. wp_op=>?; simplify_eq/=; eauto.
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 49e2160cc8642d273d41f5d4b24a6293ff2db358..c6d23574cc0f589c37a9daa0329cc67094a05e2a 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -68,7 +68,7 @@ Lemma demo_5 (M : ucmraT) (x y : M) (P : uPred M) :
 Proof.
   iIntros "H1 H2".
   iRewrite (uPred.eq_sym x x with "[#]"); first done.
-  iRewrite -("H1" $! _ with "[#]"); first done.
+  iRewrite -("H1" $! _ with "[-]"); first done.
   done.
 Qed.