diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index af764cb9e285ece79c6749bb1d9f22e4970cc3cc..ea0886873334e7318a776f7e933da8795073ea44 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -1991,34 +1991,30 @@ Tactic Notation "iRevertIntros" "(" ident(x1) ident(x2) ident(x3) ident(x4)
     ident(x12) ident(x13) ident(x14) ident(x15) ")" "with" tactic3(tac):=
   iRevertIntros (x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15) "" with tac.
 
-(** * Destruct tactic *)
-Class CopyDestruct {PROP : bi} (P : PROP).
-Arguments CopyDestruct {_} _%I.
-Global Hint Mode CopyDestruct + ! : typeclass_instances.
-
-Instance copy_destruct_forall {PROP : bi} {A} (Φ : A → PROP) : CopyDestruct (∀ x, Φ x) := {}.
-Instance copy_destruct_impl {PROP : bi} (P Q : PROP) :
-  CopyDestruct Q → CopyDestruct (P → Q) := {}.
-Instance copy_destruct_wand {PROP : bi} (P Q : PROP) :
-  CopyDestruct Q → CopyDestruct (P -∗ Q) := {}.
-Instance copy_destruct_affinely {PROP : bi} (P : PROP) :
-  CopyDestruct P → CopyDestruct (<affine> P) := {}.
-Instance copy_destruct_persistently {PROP : bi} (P : PROP) :
-  CopyDestruct P → CopyDestruct (<pers> P) := {}.
-
+(** * Destruct and PoseProof tactics *)
+(** The tactics [iDestruct] and [iPoseProof] are similar, but there are some
+subtle differences:
+
+1. The [iDestruct] tactic can be called with a natural number [n] instead of a
+   hypothesis/lemma, i.e., [iDestruct n as ...]. This introduces [n] hypotheses,
+   and then calls [iDestruct] on the last introduced hypothesis. The
+   [iPoseProof] tactic does not support this feature.
+2. When the argument [lem] of [iDestruct lem as ...] is a proof mode identifier
+   (instead of a proof mode term, i.e., no quantifiers or wands/implications are
+   eliminated), then the original hypothesis will always be removed. For
+   example, calling [iDestruct "H" as ...] on ["H" : P ∨ Q] will remove ["H"].
+   Conversely, [iPoseProof] always tries to keep the hypothesis. For example,
+   calling [iPoseProof "H" as ...] on ["H" : P ∨ Q] will keep ["H"] if it
+   resides in the intuitionistic context.
+
+These differences are also present in Coq's [destruct] and [pose proof] tactics.
+However, Coq's [destruct lem as ...] is more eager on removing the original
+hypothesis, it might also remove the original hypothesis if [lem] is not an
+identifier, but an applied term. For example, calling [destruct (H HP) as ...]
+on [H : P → Q] and [HP : P] will remove [H]. The [iDestruct] does not do this
+because it could lead to information loss if [H] resides in the intuitionistic
+context and [HP] resides in the spatial context. *)
 Tactic Notation "iDestructCore" open_constr(lem) "as" constr(p) tactic3(tac) :=
-  let ident :=
-    lazymatch type of lem with
-    | ident => constr:(Some lem)
-    | string => constr:(Some (INamed lem))
-    | iTrm =>
-       lazymatch lem with
-       | @iTrm ident ?H _ _ => constr:(Some H)
-       | @iTrm string ?H _ _ => constr:(Some (INamed H))
-       | _ => constr:(@None ident)
-       end
-    | _ => constr:(@None ident)
-    end in
   let intro_destruct n :=
     let rec go n' :=
       lazymatch n' with
@@ -2029,32 +2025,14 @@ Tactic Notation "iDestructCore" open_constr(lem) "as" constr(p) tactic3(tac) :=
     intros; go n in
   lazymatch type of lem with
   | nat => intro_destruct lem
-  | Z => (* to make it work in Z_scope. We should just be able to bind
-     tactic notation arguments to notation scopes. *)
+  | Z =>
+     (** This case is used to make the tactic work in [Z_scope]. It would be
+     better if we could bind tactic notation arguments to notation scopes, but
+     that is not supported by Ltac. *)
      let n := eval compute in (Z.to_nat lem) in intro_destruct n
-  | _ =>
-     (* Only copy the hypothesis in case there is a [CopyDestruct] instance.
-     Also, rule out cases in which it does not make sense to copy, namely when
-     destructing a lemma (instead of a hypothesis) or a spatial hypothesis
-     (which cannot be kept). *)
-     iStartProof;
-     lazymatch ident with
-     | None => iPoseProofCore lem as p tac
-     | Some ?H =>
-        lazymatch iTypeOf H with
-        | None =>
-          let H := pretty_ident H in
-          fail "iDestruct:" H "not found"
-        | Some (true, ?P) =>
-           (* intuitionistic hypothesis, check for a CopyDestruct instance *)
-           tryif (let dummy := constr:(_ : CopyDestruct P) in idtac)
-           then (iPoseProofCore lem as p tac)
-           else (iSpecializeCore lem as p; [..| tac H])
-        | Some (false, ?P) =>
-           (* spatial hypothesis, cannot copy *)
-           iSpecializeCore lem as p; [..| tac H ]
-        end
-     end
+  | ident => tac lem
+  | string => tac constr:(INamed lem)
+  | _ => iPoseProofCore lem as p tac
   end.
 
 Tactic Notation "iDestruct" open_constr(lem) "as" constr(pat) :=
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index bbaf4e29726e4e07331b9210bbc3d9716e7f065a..ba95cf6eafae0a4381f282779d438d22e936cb63 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -534,7 +534,7 @@ Tactic failure: iModIntro: spatial context is non-empty.
 "iDestruct_bad_name"
      : string
 The command has indeed failed with message:
-Tactic failure: iDestruct: "HQ" not found.
+Tactic failure: iRename: "HQ" not found.
 "iIntros_dup_name"
      : string
 The command has indeed failed with message:
diff --git a/tests/proofmode.v b/tests/proofmode.v
index ef03c12c62b126ee37d59b23a0af8adf99c3c67b..40014774004ed2599faaf153d3f054e3f125f0f3 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -93,6 +93,52 @@ Lemma test_iDestruct_intuitionistic_2 P Q `{!Persistent P, !Affine P}:
   Q ∗ (Q -∗ P) -∗ P.
 Proof. iIntros "[HQ HQP]". iDestruct ("HQP" with "HQ") as "#HP". done. Qed.
 
+Lemma test_iDestruct_specialize_wand P Q :
+  Q -∗ Q -∗ □ (Q -∗ P) -∗ P ∗ P.
+Proof.
+  iIntros "HQ1 HQ2 #HQP".
+  (* [iDestruct] does not consume "HQP" because a wand is instantiated *)
+  iDestruct ("HQP" with "HQ1") as "HP1".
+  iDestruct ("HQP" with "HQ2") as "HP2".
+  iFrame.
+Qed.
+Lemma test_iPoseProof_specialize_wand P Q :
+  Q -∗ Q -∗ □ (Q -∗ P) -∗ P ∗ P.
+Proof.
+  iIntros "HQ1 HQ2 #HQP".
+  (* [iPoseProof] does not consume "HQP" because a wand is instantiated *)
+  iPoseProof ("HQP" with "HQ1") as "HP1".
+  iPoseProof ("HQP" with "HQ2") as "HP2".
+  iFrame.
+Qed.
+
+Lemma test_iDestruct_pose_forall (Φ : nat → PROP) :
+  □ (∀ x, Φ x) -∗ Φ 0 ∗ Φ 1.
+Proof.
+  iIntros "#H".
+  (* [iDestruct] does not consume "H" because quantifiers are instantiated *)
+  iDestruct ("H" $! 0) as "$".
+  iDestruct ("H" $! 1) as "$".
+Qed.
+
+Lemma test_iDestruct_or P Q : □ (P ∨ Q) -∗ Q ∨ P.
+Proof.
+  iIntros "#H".
+  (* [iDestruct] consumes "H" because no quantifiers/wands are instantiated *)
+  iDestruct "H" as "[H|H]".
+  - by iRight.
+  - by iLeft.
+Qed.
+Lemma test_iPoseProof_or P Q : □ (P ∨ Q) -∗ (Q ∨ P) ∗ (P ∨ Q).
+Proof.
+  iIntros "#H".
+  (* [iPoseProof] does not consume "H" despite that no quantifiers/wands are
+  instantiated. This makes it different from [iDestruct]. *)
+  iPoseProof "H" as "[HP|HQ]".
+  - iFrame "H". by iRight.
+  - iFrame "H". by iLeft.
+Qed.
+
 Lemma test_iDestruct_intuitionistic_affine_bi `{!BiAffine PROP} P Q `{!Persistent P}:
   Q ∗ (Q -∗ P) -∗ P ∗ Q.
 Proof. iIntros "[HQ HQP]". iDestruct ("HQP" with "HQ") as "#HP". by iFrame. Qed.