diff --git a/CHANGELOG.md b/CHANGELOG.md
index 89a56d93933ee73bd0ec370a5b423228d182635f..9ea121fed6d674abc9ecebe4595c7cc8aabf4d76 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -30,7 +30,7 @@ lemma.
 * Add support for pure names `%H` in intro patterns. This is now natively
   supported whereas the previous experimental support required installing
   https://gitlab.mpi-sws.org/iris/string-ident.
-* Add support for destructing existentials with the intro pattern `[% ...]`.
+* Add support for destructing existentials with the intro pattern `[%x ...]`.
 
 **Changes in `base_logic`:**
 
diff --git a/docs/proof_mode.md b/docs/proof_mode.md
index b1a84922bdbba41452f6f70cbca9c4e96f01b713..0727473459417af765e997c0cdc8fa16654ee18f 100644
--- a/docs/proof_mode.md
+++ b/docs/proof_mode.md
@@ -328,19 +328,15 @@ _introduction patterns_:
   + Either the proposition `P` or `Q` should be persistent.
   + Either `ipat1` or `ipat2` should be `_`, which results in one of the
     conjuncts to be thrown away.
-- `[% ipat]` : existential elimination. Falls back to (separating) conjunction
-  elimination in case the hypothesis is not an existential, so this pattern also
-  works for (separating) conjunctions with a pure left-hand side.
+- `[%x ipat]`/`[% ipat]` : existential elimination, naming the witness `x` or
+  keeping it anonymous. Falls back to (separating) conjunction elimination in
+  case the hypothesis is not an existential, so this pattern also works for
+  (separating) conjunctions with a pure left-hand side.
 - `(pat1 & pat2 & ... & patn)` : syntactic sugar for `[pat1 [pat2 .. patn ..]]`
   to destruct nested (separating) conjunctions.
 - `[ipat1|ipat2]` : disjunction elimination.
 - `[]` : false elimination.
-- `%H` : move the hypothesis to the pure Coq context, and name it `H`. Support
-  for the `%H` introduction pattern requires an implementation of the hook
-  `string_to_ident`. Without an implementation of this hook, the `%H` pattern
-  will fail. We provide an implementation of the hook using Ltac2, which works
-  with Coq 8.11 and later, and can be installed with opam; see
-  [iris/string-ident](https://gitlab.mpi-sws.org/iris/string-ident) for details.
+- `%H` : move the hypothesis to the pure Coq context, and name it `H`.
 - `%` : move the hypothesis to the pure Coq context (anonymously). Note that if
   `%` is followed by an identifier, and not another token, a space is needed
   to disambiguate from `%H` above.
diff --git a/iris/proofmode/class_instances.v b/iris/proofmode/class_instances.v
index d28a5f9d170475c0b38116dfaf7a54c5a13f20c7..9b02c46479e100939616500a66ac1176d55fb165 100644
--- a/iris/proofmode/class_instances.v
+++ b/iris/proofmode/class_instances.v
@@ -807,12 +807,12 @@ Proof. rewrite /IntoExist=> HP. by rewrite HP affinely_exist. Qed.
 Global Instance into_exist_intuitionistically {A} P (Φ : A → PROP) name :
   IntoExist P Φ name → IntoExist (□ P) (λ a, □ (Φ a))%I name.
 Proof. rewrite /IntoExist=> HP. by rewrite HP intuitionistically_exist. Qed.
-(* This instance is generalized to let us use [iIntros (P) "..."] and
-[as [% ...]]. There is some risk of backtracking here, but that should only
-happen in failing cases (assuming that appropriate modality commuting instances
-are provided for both conjunctions and existential quantification). The
-alternative of providing specialized instances for cases like ⌜P ∧ Q⌝ turned out
-to not be tenable.
+(* This instance is generalized to let us use [iDestruct as (P) "..."] and
+[iIntros "[% ...]"] for conjunctions with a pure left-hand side. There is some
+risk of backtracking here, but that should only happen in failing cases
+(assuming that appropriate modality commuting instances are provided for both
+conjunctions and existential quantification). The alternative of providing
+specialized instances for cases like ⌜P ∧ Q⌝ turned out to not be tenable.
 
 [to_ident_name H] makes the default name [H] when [P] is destructed with
 [iExistDestruct]. See [IntoPureT] for why [φ] is a [Type]. *)
diff --git a/iris/proofmode/classes.v b/iris/proofmode/classes.v
index 74472b17b9e072ba3c8f430d718015655964a1b6..b0043325416073824d75292a1d56b63934b7b208 100644
--- a/iris/proofmode/classes.v
+++ b/iris/proofmode/classes.v
@@ -176,9 +176,9 @@ Global Arguments from_and {_} _%I _%I _%I {_}.
 Global Hint Mode FromAnd + ! - - : typeclass_instances.
 Global Hint Mode FromAnd + - ! ! : typeclass_instances. (* For iCombine *)
 
-(** The [IntoAnd p P Q1 Q2] class is used (together with [IntoSep]) to handle
-[[H1 H2]] destruct patterns. If [p] is [true] then the destruct is happening in
-the intuitionistic context.
+(** The [IntoAnd p P Q1 Q2] class is used to handle [[H1 H2]] intro patterns in
+the intuitionistic context ([p = true]) and patterns where one of the two sides
+is discarded ([p = false]).
 
 The inputs are [p P] and the outputs are [Q1 Q2]. *)
 Class IntoAnd {PROP : bi} (p : bool) (P Q1 Q2 : PROP) :=
@@ -187,8 +187,8 @@ Global Arguments IntoAnd {_} _ _%I _%I _%I : simpl never.
 Global Arguments into_and {_} _ _%I _%I _%I {_}.
 Global Hint Mode IntoAnd + + ! - - : typeclass_instances.
 
-(** The [IntoSep P Q1 Q2] class is used (together with [IntoAnd]) to handle
-[[H1 H2]] destruct patterns.
+(** The [IntoSep P Q1 Q2] class is used to handle [[H1 H2]] intro patterns in
+the spatial context (except when one side is [_], then [IntoAnd] is used).
 
 The input is [P] and the outputs are [Q1 Q2]. *)
 Class IntoSep {PROP : bi} (P Q1 Q2 : PROP) :=