diff --git a/iris/proofmode/ident_name.v b/iris/proofmode/ident_name.v
index a254743fb3e954747cb7b9f468d3d16828ead24c..ac71d5d06dc5760982c5de10a3edcef8f33e026b 100644
--- a/iris/proofmode/ident_name.v
+++ b/iris/proofmode/ident_name.v
@@ -15,14 +15,13 @@ Ltac to_ident_name id :=
     [ident_name] literals. *)
 Notation to_ident_name id := (λ id:unit, id) (only parsing).
 
-(** The idea of [AsIdentName] is to convert the binder in [f], which should be a
-    lambda, to an [ident_name] representing the name of the binder. It has only
-    one instance, a [Hint Extern] which implements that conversion to resolve
-    [name] in Ltac (see [solve_as_ident_name]).
+(** The idea of [AsIdentName] is to convert the binder in [f] to an [ident_name]
+representing the name of the binder. If [f] is not a lambda, this typeclass can
+produce the fallback identifier [__unknown]. For example, if the user writes
+[bi_exist Φ], there is no binder anywhere to extract.
 
-    This typeclass can produce the fallback identifier [__unknown] when applied
-    to an identifier rather than a lambda; for example, if the user writes
-    [bi_exist Φ], there is no binder anywhere to extract. *)
+This class has only one instance, a [Hint Extern] which implements that
+conversion to resolve [name] in Ltac (see [solve_as_ident_name]). *)
 Class AsIdentName {A B} (f : A → B) (name : ident_name) := as_ident_name {}.
 Global Arguments as_ident_name {A B f} name : assert.
 
@@ -34,7 +33,10 @@ Ltac solve_as_ident_name :=
   | |- AsIdentName (λ H, _) _ =>
     let name := to_ident_name H in
     notypeclasses refine (as_ident_name name)
-  | _ => notypeclasses refine (to_ident_name __unknown)
+  | |- AsIdentName _ _ =>
+     let name := to_ident_name ident:(__unknown) in
+     notypeclasses refine (as_ident_name name)
+  | |- _ => fail "solve_as_ident_name: goal should be `AsIdentName`"
   end.
 
 Global Hint Extern 1 (AsIdentName _ _) => solve_as_ident_name : typeclass_instances.
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index cee756d7f56d5af9e29c6bb9b86337580aa921f9..3520a7b0bf26defc0a17370c00afb95082757b91 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -101,6 +101,40 @@ Tactic failure: iExistDestruct: cannot destruct P.
   "HΦ" : ∃ x : nat, Φ x
   --------------------------------------∗
   ∃ x : nat, Φ x
+"test_iDestruct_nameless_exist"
+     : string
+1 goal
+  
+  PROP : bi
+  Φ : nat → PROP
+  __unknown : nat
+  ============================
+  "H" : Φ __unknown
+  --------------------------------------∗
+  ∃ x : nat, Φ x
+"test_iIntros_nameless_forall"
+     : string
+1 goal
+  
+  PROP : bi
+  Φ : nat → PROP
+  __unknown : nat
+  ============================
+  "H" : ∀ x : nat, Φ x
+  --------------------------------------∗
+  Φ __unknown
+"test_iIntros_nameless_pure_forall"
+     : string
+1 goal
+  
+  PROP : bi
+  BiPureForall0 : BiPureForall PROP
+  φ : nat → Prop
+  __unknown : nat
+  ============================
+  "H" : ∀ x : nat, ⌜φ x⌝
+  --------------------------------------∗
+  ⌜φ __unknown⌝
 "test_iIntros_forall_pure"
      : string
 1 goal
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 5e06d6df43253007fbd4e493130f87a9ff6af086..f7008326a1527981aacf226383f41177106bb5b0 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -266,6 +266,21 @@ Qed.
 Lemma test_iIntros_pure (ψ φ : Prop) P : ψ → ⊢ ⌜ φ ⌝ → P → ⌜ φ ∧ ψ ⌝ ∧ P.
 Proof. iIntros (??) "H". auto. Qed.
 
+(** The following tests check that [AsIdentName Φ ?name] works for the case
+that [Φ] is not a lambda, but a variable. It should use name [__unknown]. *)
+Check "test_iDestruct_nameless_exist".
+Lemma test_iDestruct_nameless_exist (Φ : nat → PROP) :
+  bi_exist Φ ⊢@{PROP} ∃ x, Φ x.
+Proof. iDestruct 1 as (?) "H". Show. auto. Qed.
+Check "test_iIntros_nameless_forall".
+Lemma test_iIntros_nameless_forall (Φ : nat → PROP) :
+  (∀ x, Φ x) ⊢@{PROP} bi_forall Φ.
+Proof. iIntros "H" (?). Show. done. Qed.
+Check "test_iIntros_nameless_pure_forall".
+Lemma test_iIntros_nameless_pure_forall `{!BiPureForall PROP} (φ : nat → Prop) :
+  (∀ x, ⌜ φ x ⌝) ⊢@{PROP} ⌜ ∀ x, φ x ⌝.
+Proof. iIntros "H" (?). Show. done. Qed.
+
 Check "test_iIntros_forall_pure".
 Lemma test_iIntros_forall_pure (Ψ: nat → PROP) :
   ⊢ ∀ x : nat, Ψ x → Ψ x.