diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index 41453a3a76f3b0ce78aa535faf659ee8675442ff..7d76d952d6de5c740c3c5813601736fd55b061a7 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -1476,7 +1476,8 @@ Tactic Notation "iModCore" constr(H) "as" constr(H') :=
    to the intro-pattern [pat], when trying to avoid extra renamings. These
    mainly look whether the pattern is a name, and use that name in that case.
    Otherwise, [ident_for_pat] generates a fresh name (a safe option), and
-   [ident_for_pat_default] uses the [default] name that it was provided.
+   [ident_for_pat_default] uses the [default] name that it was provided if
+   it is an anonymous name.
 *)
 Local Ltac ident_for_pat pat :=
   lazymatch pat with
@@ -1487,7 +1488,11 @@ Local Ltac ident_for_pat pat :=
 Local Ltac ident_for_pat_default pat default :=
   lazymatch pat with
   | IIdent ?x => x
-  | _ => default
+  | _ =>
+    lazymatch default with
+    | IAnon _ => default
+    | _ => let x := iFresh in x
+    end
   end.
 
 (** [pat0] is the unparsed pattern, and is only used in error messages *)
@@ -1526,22 +1531,11 @@ Local Ltac iDestructHypGo Hz pat0 pat :=
      rename_by_string x s;
      iDestructHypGo y pat0 pat2
   | IList [[?pat1; ?pat2]] =>
-     (* We have to take care of not using the same name for the two hypotheses.
-        Furthermore, we can only reuse the name [Hz] for the first hypothesis,
-        on which we recurse first.
-
-        One tricky case is iDestruct "H" as "[? H]": here, we cannot reuse the
-        name "H" for the first hypothesis, as it would clash with the chosen
-        name for the second one. Hence, we need to compute the second name
-        first, and check it against [Hz] to know if it can be reused.
-      *)
+     (* We have to take care of not using the same name for the two hypotheses:
+        [ident_for_pat_default] will thus only reuse [Hz] (which could in principle
+        clash with a name from [pat2]) if it is an anonymous name. *)
+     let x1 := ident_for_pat_default pat1 Hz in
      let x2 := ident_for_pat pat2 in
-     let x1 :=
-       lazymatch x2 with
-       | Hz => ident_for_pat pat1
-       | _ => ident_for_pat_default pat1 Hz
-       end
-     in
      iAndDestruct Hz as x1 x2;
      iDestructHypGo x1 pat0 pat1; iDestructHypGo x2 pat0 pat2
   | IList [_ :: _ :: _] => fail "iDestruct:" pat0 "has too many conjuncts"