diff --git a/ProofMode.md b/ProofMode.md
index 773baa3fff414ee1212212d4942f3ef9ee76b3c9..dbbe030f4356c58bbb2452006c566fa0989e5abf 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -39,8 +39,10 @@ Context management
   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`.
+- `iPoseProof pm_trm as (x1 ... xn) "ipat"` : put `pm_trm` into the context and
+  eliminates it. This tactic is essentially the same as `iDestruct` with the
+  difference that when `pm_trm` is a non-univerisally quantified spatial
+  hypothesis, it will not throw the hypothesis away.
 - `iAssert P with "spat" as "ipat"` : generates a new subgoal `P` and adds the
   hypothesis `P` to the current goal. The specialization pattern `spat`
   specifies which hypotheses will be consumed by proving `P`. The introduction
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 7ad7a193a58595650ecc743641f057fea74efbb5..89c42bdc7c0c11e21bc679fd74d8ed0909750155 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -554,9 +554,6 @@ Tactic Notation "iPoseProofCore" open_constr(lem)
   | false => go spec_tac; last (tac Htmp)
   end.
 
-Tactic Notation "iPoseProof" open_constr(lem) "as" constr(H) :=
-  iPoseProofCore lem as false false (fun Htmp => iRename Htmp into H).
-
 (** * Apply *)
 Tactic Notation "iApply" open_constr(lem) :=
   let rec go H := first
@@ -1172,6 +1169,40 @@ Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1)
 Tactic Notation "iDestruct" open_constr(lem) "as" "%" simple_intropattern(pat) :=
   iDestructCore lem as true (fun H => iPure H as pat).
 
+Tactic Notation "iPoseProof" open_constr(lem) "as" constr(pat) :=
+  iPoseProofCore lem as pat false (fun H => iDestructHyp H as pat).
+Tactic Notation "iPoseProof" open_constr(lem) "as" "(" simple_intropattern(x1) ")"
+    constr(pat) :=
+  iPoseProofCore lem as pat false (fun H => iDestructHyp H as ( x1 ) pat).
+Tactic Notation "iPoseProof" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) ")" constr(pat) :=
+  iPoseProofCore lem as pat false (fun H => iDestructHyp H as ( x1 x2 ) pat).
+Tactic Notation "iPoseProof" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) ")" constr(pat) :=
+  iPoseProofCore lem as pat false (fun H => iDestructHyp H as ( x1 x2 x3 ) pat).
+Tactic Notation "iPoseProof" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
+    constr(pat) :=
+  iPoseProofCore lem as pat false (fun H => iDestructHyp H as ( x1 x2 x3 x4 ) pat).
+Tactic Notation "iPoseProof" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
+    simple_intropattern(x5) ")" constr(pat) :=
+  iPoseProofCore lem as pat false (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 ) pat).
+Tactic Notation "iPoseProof" open_constr(lem) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
+    simple_intropattern(x5) simple_intropattern(x6) ")" constr(pat) :=
+  iPoseProofCore lem as pat false (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 ) pat).
+Tactic Notation "iPoseProof" 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) :=
+  iPoseProofCore lem as pat false (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 ) pat).
+Tactic Notation "iPoseProof" 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) :=
+  iPoseProofCore lem as pat false (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat).
+
 (** * Induction *)
 Tactic Notation "iInductionCore" constr(x)
     "as" simple_intropattern(pat) constr(IH) :=