diff --git a/docs/proof_mode.md b/docs/proof_mode.md
index dca9f23dfaa650de2f0c191b7929ae0c27bba143..81bcfff80fbe94946d1a4d4020df6078bb9a2b55 100644
--- a/docs/proof_mode.md
+++ b/docs/proof_mode.md
@@ -259,6 +259,7 @@ _introduction patterns_:
   tactic is a no-op. If the hypothesis is not affine, an `<affine>` modality is
   added to the hypothesis.
 - `> ipat` : eliminate a modality (if the goal permits).
+- `H.ipat` : prepend the name `H` to all names appearing in `ipat`.
 
 Apart from this, there are the following introduction patterns that can only
 appear at the top level:
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 901ac767ece923854da73e679a568509dba42ab4..647d768c6feea56e4a5bf3224cde2e058d35589e 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -919,6 +919,16 @@ Lemma test_iDestruct_clear P Q R :
 Proof.
   iIntros "HP HQR". iDestruct "HQR" as "{HP} [HQ HR]". done.
 Qed.
+
+Lemma test_iDestruct_prepend_1 P Q :
+  P ∗ Q -∗ Q ∗ P.
+Proof. iIntros "H.[P Q]". iFrame "HP HQ". Qed.
+Lemma test_iDestruct_prepend_2 P Q :
+  P ∗ Q -∗ Q ∗ P.
+Proof. iIntros "H.[P ?]". by iFrame "HP". Qed.
+Lemma test_iDestruct_prepend_3 P Q :
+  P ∗ Q -∗ Q ∗ P.
+Proof. iIntros "H.H.[P Q]". by iFrame "HHP". Qed.
 End tests.
 
 Section parsing_tests.
@@ -1266,4 +1276,11 @@ Proof.
   Fail iIntros "[H %H]".
 Abort.
 
+Lemma test_iDestruct_pure_prepend_1 φ :
+  ⌜ φ ⌝ ⊢@{PROP} ⌜ φ ⌝.
+Proof. iIntros "H.%P2". iPureIntro. exact HP2. Qed.
+Lemma test_iDestruct_pure_prepend_2 P φ :
+  P ∗ ⌜ φ ⌝ -∗ ⌜ φ ⌝ ∗ P.
+Proof. iIntros "H.[$ %P2]". iPureIntro. exact HP2. Qed.
+
 End pure_name_tests.
diff --git a/theories/proofmode/intro_patterns.v b/theories/proofmode/intro_patterns.v
index 1d3cb9922fbcf41d9f08a6227a81ac6ed649e46b..af0789c8ca77f926462a5310140f110e973a9d75 100644
--- a/theories/proofmode/intro_patterns.v
+++ b/theories/proofmode/intro_patterns.v
@@ -17,6 +17,7 @@ Inductive intro_pat :=
   | ISpatial : intro_pat → intro_pat
   | IModalElim : intro_pat → intro_pat
   | IRewrite : direction → intro_pat
+  | IPrepend : string → intro_pat → intro_pat
   | IPureIntro : intro_pat
   | IModalIntro : intro_pat
   | ISimpl : intro_pat
@@ -35,7 +36,8 @@ Inductive stack_item :=
   | StAmp : stack_item
   | StIntuitionistic : stack_item
   | StSpatial : stack_item
-  | StModalElim : stack_item.
+  | StModalElim : stack_item
+  | StPrepend : string → stack_item.
 Notation stack := (list stack_item).
 
 Fixpoint close_list (k : stack)
@@ -47,6 +49,8 @@ Fixpoint close_list (k : stack)
      '(p,ps) ← maybe2 (::) ps; close_list k (IIntuitionistic p :: ps) pss
   | StModalElim :: k =>
      '(p,ps) ← maybe2 (::) ps; close_list k (IModalElim p :: ps) pss
+  | StPrepend s :: k =>
+     '(p,ps) ← maybe2 (::) ps; close_list k (IPrepend s p :: ps) pss
   | StBar :: k => close_list k [] (ps :: pss)
   | _ => None
   end.
@@ -71,6 +75,7 @@ Fixpoint close_conj_list (k : stack)
   | StIntuitionistic :: k => p ← cur; close_conj_list k (Some (IIntuitionistic p)) ps
   | StSpatial :: k => p ← cur; close_conj_list k (Some (ISpatial p)) ps
   | StModalElim :: k => p ← cur; close_conj_list k (Some (IModalElim p)) ps
+  | StPrepend s :: k => p ← cur; close_conj_list k (Some (IPrepend s p)) ps
   | StAmp :: k => p ← cur; close_conj_list k None (p :: ps)
   | _ => None
   end.
@@ -78,6 +83,7 @@ Fixpoint close_conj_list (k : stack)
 Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
   match ts with
   | [] => Some k
+  | TName s :: TDot :: ts => parse_go ts (StPrepend s :: k)
   | TName "_" :: ts => parse_go ts (StPat IDrop :: k)
   | TName s :: ts => parse_go ts (StPat (IIdent s) :: k)
   | TAnon :: ts => parse_go ts (StPat IFresh :: k)
@@ -124,6 +130,7 @@ Fixpoint close (k : stack) (ps : list intro_pat) : option (list intro_pat) :=
   | StIntuitionistic :: k => '(p,ps) ← maybe2 (::) ps; close k (IIntuitionistic p :: ps)
   | StSpatial :: k => '(p,ps) ← maybe2 (::) ps; close k (ISpatial p :: ps)
   | StModalElim :: k => '(p,ps) ← maybe2 (::) ps; close k (IModalElim p :: ps)
+  | StPrepend s :: k => '(p,ps) ← maybe2 (::) ps; close k (IPrepend s p :: ps)
   | _ => None
   end.
 
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 4042d85e566161da21b30239fda57732741bb477..21bfd136731e9234b2693e041e0289fcd56f4f1d 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -1415,7 +1415,7 @@ Local Ltac string_to_ident s :=
   end.
 
 (** * Basic destruct tactic *)
-Local Ltac iDestructHypGo Hz pat :=
+Local Ltac iDestructHypGo Hacc Hz pat :=
   lazymatch pat with
   | IFresh =>
      lazymatch Hz with
@@ -1424,21 +1424,33 @@ Local Ltac iDestructHypGo Hz pat :=
      end
   | IDrop => iClearHyp Hz
   | IFrame => iFrameHyp Hz
-  | IIdent ?y => iRename Hz into y
+  | IIdent ?H =>
+     lazymatch H with
+     | IAnon ?n => iRename Hz into (IAnon n)
+     | INamed ?H => let H := eval cbv in (Hacc +:+ H) in iRename Hz into (INamed H)
+     end
   | IList [[]] => iExFalso; iExact Hz
-  | IList [[?pat1; IDrop]] => iAndDestructChoice Hz as Left Hz; iDestructHypGo Hz pat1
-  | IList [[IDrop; ?pat2]] => iAndDestructChoice Hz as Right Hz; iDestructHypGo Hz pat2
+  | IList [[?pat1; IDrop]] => iAndDestructChoice Hz as Left Hz; iDestructHypGo Hacc Hz pat1
+  | IList [[IDrop; ?pat2]] => iAndDestructChoice Hz as Right Hz; iDestructHypGo Hacc Hz pat2
   | IList [[?pat1; ?pat2]] =>
-     let Hy := iFresh in iAndDestruct Hz as Hz Hy; iDestructHypGo Hz pat1; iDestructHypGo Hy pat2
-  | IList [[?pat1];[?pat2]] => iOrDestruct Hz as Hz Hz; [iDestructHypGo Hz pat1|iDestructHypGo Hz pat2]
+     let Hy := iFresh in iAndDestruct Hz as Hz Hy;
+     iDestructHypGo Hacc Hz pat1; iDestructHypGo Hacc Hy pat2
+  | IList [[?pat1];[?pat2]] =>
+     iOrDestruct Hz as Hz Hz;
+       [iDestructHypGo Hacc Hz pat1|iDestructHypGo Hacc Hz pat2]
   | IPure IGallinaAnon => iPure Hz as ?
-  | IPure (IGallinaNamed ?s) => let x := string_to_ident s in
-                                iPure Hz as x
+  | IPure (IGallinaNamed ?s) =>
+     let s := eval cbv in (Hacc +:+ s) in
+     let x := string_to_ident s in
+     iPure Hz as x
   | IRewrite Right => iPure Hz as ->
   | IRewrite Left => iPure Hz as <-
-  | IIntuitionistic ?pat => iIntuitionistic Hz; iDestructHypGo Hz pat
-  | ISpatial ?pat => iSpatial Hz; iDestructHypGo Hz pat
-  | IModalElim ?pat => iModCore Hz; iDestructHypGo Hz pat
+  | IIntuitionistic ?pat => iIntuitionistic Hz; iDestructHypGo Hacc Hz pat
+  | ISpatial ?pat => iSpatial Hz; iDestructHypGo Hacc Hz pat
+  | IModalElim ?pat => iModCore Hz; iDestructHypGo Hacc Hz pat
+  | IPrepend ?H ?pat =>
+     let Hacc := eval cbv in (H +:+ Hacc) in
+     iDestructHypGo Hacc Hz pat
   | _ => fail "iDestruct:" pat "invalid"
   end.
 Local Ltac iDestructHypFindPat Hgo pat found pats :=
@@ -1453,7 +1465,7 @@ Local Ltac iDestructHypFindPat Hgo pat found pats :=
   | IClearFrame ?H :: ?pats => iFrame H; iDestructHypFindPat Hgo pat found pats
   | ?pat :: ?pats =>
      lazymatch found with
-     | false => iDestructHypGo Hgo pat; iDestructHypFindPat Hgo pat true pats
+     | false => iDestructHypGo "" Hgo pat; iDestructHypFindPat Hgo pat true pats
      | true => fail "iDestruct:" pat "should contain exactly one proper introduction pattern"
      end
   end.
diff --git a/theories/proofmode/tokens.v b/theories/proofmode/tokens.v
index cb3a34fbf48686d59737563b618a065be51c65c3..95b9e34626893cc18231fc2b42fd012469fb4d08 100644
--- a/theories/proofmode/tokens.v
+++ b/theories/proofmode/tokens.v
@@ -26,7 +26,8 @@ Inductive token :=
   | TAll : token
   | TMinus : token
   | TSep : token
-  | TArrow : direction → token.
+  | TArrow : direction → token
+  | TDot : token.
 
 Inductive state :=
   | SName : string → state
@@ -70,6 +71,7 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : state) : list token :=
   | String "-" (String ">" s) => tokenize_go s (TArrow Right :: cons_state kn k) SNone
   | String "<" (String "-" s) => tokenize_go s (TArrow Left :: cons_state kn k) SNone
   | String "-" s => tokenize_go s (TMinus :: cons_state kn k) SNone
+  | String "." s => tokenize_go s (TDot :: cons_state kn k) SNone
   | String (Ascii.Ascii false true false false false true true true) (* unicode ∗ *)
       (String (Ascii.Ascii false false false true false false false true)
       (String (Ascii.Ascii true true true false true false false true) s)) =>