diff --git a/ProofMode.md b/ProofMode.md
index 845d81fd334dad13799e6327ba2a05c32d1e114c..023a6d4c5ada2e32ed40f8fcb636bcb5c85227f0 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -170,11 +170,11 @@ Rewriting / simplification
 Iris
 ----
 
-- `iInv (N with "selpat") as (x1 ... xn) "ipat" "Hclose"` : open the invariant
-  `N`. The selection pattern `selpat` is used for any auxiliary assertions
-  needed to open the invariant (e.g. for cancelable or non-atomic
-  invariants). The update for closing the invariant is put in a hypothesis named
-  `Hclose`.
+- `iInv S with "selpat" as (x1 ... xn) "ipat" "Hclose"` : where `S` is either
+   a namespace N or an identifier "H". Open the invariant indicated by S.  The
+   selection pattern `selpat` is used for any auxiliary assertions needed to
+   open the invariant (e.g. for cancelable or non-atomic invariants). The update
+   for closing the invariant is put in a hypothesis named `Hclose`.
 
 Miscellaneous
 -------------
diff --git a/theories/base_logic/lib/cancelable_invariants.v b/theories/base_logic/lib/cancelable_invariants.v
index 00816bf529257aeed765c6d445c06aaf4fe35965..1d5746182d75c2fc9b6aee61950392c7efa0a94a 100644
--- a/theories/base_logic/lib/cancelable_invariants.v
+++ b/theories/base_logic/lib/cancelable_invariants.v
@@ -94,7 +94,7 @@ Section proofs.
   Global Instance into_inv_cinv N γ P : IntoInv (cinv N γ P) N.
   Global Instance elim_inv_cinv p γ E N P P' Q Q' :
     ElimModal True (|={E,E∖↑N}=> (▷ P ∗ cinv_own γ p) ∗ (▷ P ={E∖↑N,E}=∗ True))%I P' Q Q' →
-    ElimInv (↑N ⊆ E) N (cinv N γ P) (cinv_own γ p) P' Q Q'.
+    ElimInv (↑N ⊆ E) (cinv N γ P) (cinv_own γ p) P' Q Q'.
   Proof.
     rewrite /ElimInv /ElimModal. iIntros (Helim ?) "(#H1&Hown&H2)".
     iApply Helim; auto. iFrame "H2".
diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index 5237e4a0aed87da39a4b115e1d152b99db7b79a5..b183072b189e3cb323cdc8a7d27541c5073b6a9d 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -98,7 +98,7 @@ Global Instance into_inv_inv N P : IntoInv (inv N P) N.
 
 Global Instance elim_inv_inv E N P P' Q Q' :
   ElimModal True (|={E,E∖↑N}=> ▷ P ∗ (▷ P ={E∖↑N,E}=∗ True))%I P' Q Q' →
-  ElimInv (↑N ⊆ E) N (inv N P) True P' Q Q'.
+  ElimInv (↑N ⊆ E) (inv N P) True P' Q Q'.
 Proof.
   rewrite /ElimInv /ElimModal. iIntros (Helim ?) "(#H1&_&H2)".
   iApply Helim; auto; iFrame.
diff --git a/theories/base_logic/lib/na_invariants.v b/theories/base_logic/lib/na_invariants.v
index b3fe3d1e1c7b0dab659ccc9a0217d114bad5a6d1..2979b57bfe3f1892c08fcdf2fb110575bd95acaa 100644
--- a/theories/base_logic/lib/na_invariants.v
+++ b/theories/base_logic/lib/na_invariants.v
@@ -115,7 +115,7 @@ Section proofs.
   Global Instance elim_inv_na p F E N P P' Q Q':
     ElimModal True (|={E}=> (▷ P ∗ na_own p (F∖↑N)) ∗ (▷ P ∗ na_own p (F∖↑N) ={E}=∗ na_own p F))%I
               P' Q Q' →
-    ElimInv (↑N ⊆ E ∧ ↑N ⊆ F) N (na_inv p N P) (na_own p F) P' Q Q'.
+    ElimInv (↑N ⊆ E ∧ ↑N ⊆ F) (na_inv p N P) (na_own p F) P' Q Q'.
   Proof.
     rewrite /ElimInv /ElimModal. iIntros (Helim (?&?)) "(#H1&Hown&H2)".
     iApply Helim; auto. iFrame "H2".
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 3d1bb6a87fd80d74b5b43dbc36e6311c57e0679f..0e8eac3acdbced7c79dc3611d67b9255b57b4da2 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -487,11 +487,11 @@ Hint Mode IntoInv + ! - : typeclass_instances.
    is not a clearly associated instance of ElimModal of the right form
    (e.g. to handle Iris 2.0 usage of iInv).
 *)
-Class ElimInv {PROP : bi} (φ : Prop) (N : namespace) (Pinv Pin Pout Q Q' : PROP) :=
+Class ElimInv {PROP : bi} (φ : Prop) (Pinv Pin Pout Q Q' : PROP) :=
   elim_inv : φ → Pinv ∗ Pin ∗ (Pout -∗ Q') ⊢ Q.
-Arguments ElimInv {_} _ _ _  _%I _%I _%I _%I : simpl never.
+Arguments ElimInv {_} _ _ _%I _%I _%I _%I : simpl never.
 Arguments elim_inv {_} _ _ _%I _%I _%I _%I _%I _%I.
-Hint Mode ElimInv + - - ! - - - - : typeclass_instances.
+Hint Mode ElimInv + - ! - - - - : typeclass_instances.
 
 (* We make sure that tactics that perform actions on *specific* hypotheses or
 parts of the goal look through the [tc_opaque] connective, which is used to make
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 75d763eadb4d7d5aa033626ba670c88e4f3be6e5..7e3bf94bc4bac314958c057cb76de610bb083009 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -1171,9 +1171,9 @@ Proof.
 Qed.
 
 (** * Invariants *)
-Lemma tac_inv_elim Δ Δ' i j φ N p P Pin Pout Q Q' :
+Lemma tac_inv_elim Δ Δ' i j φ p P Pin Pout Q Q' :
   envs_lookup_delete false i Δ = Some (p, P, Δ') →
-  ElimInv φ N P Pin Pout Q Q' →
+  ElimInv φ P Pin Pout Q Q' →
   φ →
   (∀ R, ∃ Δ'',
     envs_app false (Esnoc Enil j (Pin -∗ (Pout -∗ Q') -∗ R)%I) Δ' = Some Δ'' ∧
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 59945b400d9f4166b631ce63d65adcde1727f3b0..dd7935ca43d055dfee9342df740f112f37002924 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -1865,7 +1865,7 @@ Tactic Notation "iMod" open_constr(lem) "as" "(" simple_intropattern(x1)
 Tactic Notation "iMod" open_constr(lem) "as" "%" simple_intropattern(pat) :=
   iDestructCore lem as false (fun H => iModCore H; iPure H as pat).
 
-(** * Assert *)
+(** * Invariant *)
 
 (* Finds a hypothesis in the context that is an invariant with
    namespace [N].  To do so, we check whether for each hypothesis
@@ -1874,7 +1874,8 @@ Tactic Notation "iAssumptionInv" constr(N) :=
   let rec find Γ i P :=
     lazymatch Γ with
     | Esnoc ?Γ ?j ?P' =>
-      first [assert (IntoInv P' N) by apply _; unify P P'; unify i j|find Γ i P]
+      first [(let H := constr:(_: IntoInv P' N) in
+             unify P P'; unify i j)|find Γ i P]
     end in
   match goal with
   | |- envs_lookup_delete _ ?i (Envs ?Γp ?Γs) = Some (_, ?P, _) =>
@@ -1883,14 +1884,31 @@ Tactic Notation "iAssumptionInv" constr(N) :=
      is_evar i; first [find Γp i P | find Γs i P]; env_reflexivity
   end.
 
-Tactic Notation "iInvCore" constr(N) "with" constr(pats) "as" tactic(tac) constr(Hclose) :=
+(* The argument [select] is the namespace [N] or hypothesis name ["H"] of the
+invariant. *)
+Tactic Notation "iInvCore" constr(select) "with" constr(pats) "as" tactic(tac) constr(Hclose) :=
   iStartProof;
+  let pats := spec_pat.parse pats in
+  lazymatch pats with
+  | [_] => idtac
+  | _ => fail "iInv: exactly one specialization pattern should be given"
+  end;
   let H := iFresh in
-  eapply tac_inv_elim with _ _ H _ N _ _ _ _ _;
-    [iAssumptionInv N || fail "iInv: invariant" N "not found"
-    |apply _ ||
-     let I := match goal with |- ElimInv _ ?N ?I  _ _ _ _ => I end in
-     fail "iInv: cannot eliminate invariant " I " with namespace " N
+  lazymatch type of select with
+  | string =>
+     eapply tac_inv_elim with _ select H _ _ _ _ _ _;
+     first by (iAssumptionCore || fail "iInv: invariant" select "not found")
+  | ident  =>
+     eapply tac_inv_elim with _ select H _ _ _ _ _ _;
+     first by (iAssumptionCore || fail "iInv: invariant" select "not found")
+  | namespace =>
+     eapply tac_inv_elim with _ _ H _ _ _ _ _ _;
+     first by (iAssumptionInv select || fail "iInv: invariant" select "not found")
+  | _ => fail "iInv: selector" select "is not of the right type "
+  end;
+    [apply _ ||
+     let I := match goal with |- ElimInv _ ?I  _ _ _ _ => I end in
+     fail "iInv: cannot eliminate invariant " I
     |try (split_and?; solve [ fast_done | solve_ndisj ])
     |let R := fresh in intros R; eexists; split; [env_reflexivity|];
      iSpecializePat H pats; last (
@@ -1900,7 +1918,7 @@ Tactic Notation "iInvCore" constr(N) "with" constr(pats) "as" tactic(tac) constr
        let patintro := constr:(IList [[IIdent H; patclose]]) in
        iDestructHyp H as patintro;
        tac H
-     )].
+    )].
 
 Tactic Notation "iInvCore" constr(N) "as" tactic(tac) constr(Hclose) :=
   iInvCore N with "[$]" as ltac:(tac) Hclose.
diff --git a/theories/tests/proofmode_iris.v b/theories/tests/proofmode_iris.v
index 33acf1207914df8094d63fa380f8fa453fb14a61..01b80bb6a49d72be89f0fdee9e9be2df260a8b5a 100644
--- a/theories/tests/proofmode_iris.v
+++ b/theories/tests/proofmode_iris.v
@@ -144,4 +144,47 @@ Section iris_tests.
     iInv N as "HP" "Hclose".
     iMod ("Hclose" with "[$HP]"). auto.
   Qed.
+
+  (* test selection by hypothesis name instead of namespace *)
+  Lemma test_iInv_9 t N1 N2 N3 E1 E2 P:
+    ↑N3 ⊆ E1 →
+    inv N1 P ∗ na_inv t N3 (bi_persistently P) ∗ inv N2 P  ∗ na_own t E1 ∗ na_own t E2
+      ={⊤}=∗ na_own t E1 ∗ na_own t E2  ∗ ▷ P.
+  Proof.
+    iIntros (?) "(#?&#HInv&#?&Hown1&Hown2)".
+    iInv "HInv" with "Hown1" as "(#HP&Hown1)" "Hclose".
+    iMod ("Hclose" with "[$HP $Hown1]").
+    iModIntro. iFrame. by iNext.
+  Qed.
+
+  (* test selection by hypothesis name instead of namespace *)
+  Lemma test_iInv_10 t N1 N2 N3 E1 E2 P:
+    ↑N3 ⊆ E1 →
+    inv N1 P ∗ na_inv t N3 (bi_persistently P) ∗ inv N2 P  ∗ na_own t E1 ∗ na_own t E2
+      ={⊤}=∗ na_own t E1 ∗ na_own t E2  ∗ ▷ P.
+  Proof.
+    iIntros (?) "(#?&#HInv&#?&Hown1&Hown2)".
+    iInv "HInv" as "(#HP&Hown1)" "Hclose".
+    iMod ("Hclose" with "[$HP $Hown1]").
+    iModIntro. iFrame. by iNext.
+  Qed.
+
+  (* test selection by ident name *)
+  Lemma test_iInv_11 N P: inv N (bi_persistently P) ={⊤}=∗ ▷ P.
+  Proof.
+    let H := iFresh in
+    (iIntros H; iInv H as "#H2" "Hclose").
+    iMod ("Hclose" with "H2").
+    iModIntro. by iNext.
+  Qed.
+
+  (* error messages *)
+  Lemma test_iInv_12 N P: inv N (bi_persistently P) ={⊤}=∗ True.
+  Proof.
+    iIntros "H".
+    Fail iInv 34 as "#H2" "Hclose".
+    Fail iInv nroot as "#H2" "Hclose".
+    Fail iInv "H2" as "#H2" "Hclose".
+    done.
+  Qed.
 End iris_tests.