diff --git a/ProofMode.md b/ProofMode.md
index 02aabe071b0533e754b3e7a0fd38a24305b6da21..023a6d4c5ada2e32ed40f8fcb636bcb5c85227f0 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -170,8 +170,11 @@ Rewriting / simplification
 Iris
 ----
 
-- `iInv N as (x1 ... xn) "ipat" "Hclose"` : open the invariant `N`, 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/opam b/opam
index 10784bc107cf4a5a18041a337ac3f8f1d3bdb7ac..1afd1a748a5a7494c93c18824b633bd89ec7918a 100644
--- a/opam
+++ b/opam
@@ -11,5 +11,5 @@ install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
 depends: [
   "coq" { >= "8.7.1" & < "8.8~" | (= "dev") }
-  "coq-stdpp" { (= "dev.2018-02-21.0") | (= "dev") }
+  "coq-stdpp" { (= "dev.2018-02-23.0") | (= "dev") }
 ]
diff --git a/theories/base_logic/lib/cancelable_invariants.v b/theories/base_logic/lib/cancelable_invariants.v
index fa21aad639eed6efdb94f3b25e040d2f813405ad..294019faec346667934dee96b53fa88b445521d6 100644
--- a/theories/base_logic/lib/cancelable_invariants.v
+++ b/theories/base_logic/lib/cancelable_invariants.v
@@ -90,6 +90,18 @@ Section proofs.
       + iIntros "HP". iApply "Hclose". iLeft. iNext. by iApply "HP'".
     - iDestruct (cinv_own_1_l with "Hγ' Hγ") as %[].
   Qed.
+
+  Global Instance into_inv_cinv N γ P : IntoInv (cinv N γ P) N.
+  Global Instance elim_inv_cinv p γ E N P Q Q' :
+    (∀ R, ElimModal True (|={E,E∖↑N}=> R) R Q Q') →
+    ElimInv (↑N ⊆ E) (cinv N γ P) (cinv_own γ p)
+      (▷ P ∗ cinv_own γ p) (▷ P ={E∖↑N,E}=∗ True) Q Q'.
+  Proof.
+    rewrite /ElimInv /ElimModal. iIntros (Helim ?) "(#H1&Hown&H2)".
+    iApply (Helim with "[- $H2]"); first done.
+    iMod (cinv_open E N γ p P with "[#] [Hown]") as "(HP&Hown&Hclose)"; auto. 
+    by iFrame.
+  Qed.
 End proofs.
 
 Typeclasses Opaque cinv_own cinv.
diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index e99d0fe890b49c2a27b93d39f5e6dc20a1e56a06..b18cb809f590f073399ef6f2e52a443756765053 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -1,8 +1,8 @@
 From iris.base_logic.lib Require Export fancy_updates.
-From stdpp Require Export  namespaces.
+From stdpp Require Export namespaces.
 From iris.base_logic.lib Require Import wsat.
 From iris.algebra Require Import gmap.
-From iris.proofmode Require Import tactics coq_tactics intro_patterns.
+From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 Import uPred.
 
@@ -94,6 +94,17 @@ Proof.
   iApply "HP'". iFrame.
 Qed.
 
+Global Instance into_inv_inv N P : IntoInv (inv N P) N.
+
+Global Instance elim_inv_inv E N P Q Q' :
+  (∀ R, ElimModal True (|={E,E∖↑N}=> R) R Q Q') →
+  ElimInv (↑N ⊆ E) (inv N P) True (▷ P) (▷ P ={E∖↑N,E}=∗ True) Q Q'.
+Proof.
+  rewrite /ElimInv /ElimModal. iIntros (Helim ?) "(#H1&_&H2)".
+  iApply (Helim with "[$H2]"); first done.
+  iMod (inv_open _ N with "[#]") as "(HP&Hclose)"; auto with iFrame.
+Qed.
+
 Lemma inv_open_timeless E N P `{!Timeless P} :
   ↑N ⊆ E → inv N P ={E,E∖↑N}=∗ P ∗ (P ={E∖↑N,E}=∗ True).
 Proof.
@@ -101,29 +112,3 @@ Proof.
   iIntros "!> {$HP} HP". iApply "Hclose"; auto.
 Qed.
 End inv.
-
-Tactic Notation "iInvCore" constr(N) "as" tactic(tac) constr(Hclose) :=
-  let Htmp := iFresh in
-  let patback := intro_pat.parse_one Hclose in
-  let pat := constr:(IList [[IIdent Htmp; patback]]) in
-  iMod (inv_open _ N with "[#]") as pat;
-    [idtac|iAssumption || fail "iInv: invariant" N "not found"|idtac];
-    [solve_ndisj || match goal with |- ?P => fail "iInv: cannot solve" P end
-    |tac Htmp].
-
-Tactic Notation "iInv" constr(N) "as" constr(pat) constr(Hclose) :=
-   iInvCore N as (fun H => iDestructHyp H as pat) Hclose.
-Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1) ")"
-    constr(pat) constr(Hclose) :=
-   iInvCore N as (fun H => iDestructHyp H as (x1) pat) Hclose.
-Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
-    simple_intropattern(x2) ")" constr(pat) constr(Hclose) :=
-   iInvCore N as (fun H => iDestructHyp H as (x1 x2) pat) Hclose.
-Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
-    simple_intropattern(x2) simple_intropattern(x3) ")"
-    constr(pat) constr(Hclose) :=
-   iInvCore N as (fun H => iDestructHyp H as (x1 x2 x3) pat) Hclose.
-Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
-    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
-    constr(pat) constr(Hclose) :=
-   iInvCore N as (fun H => iDestructHyp H as (x1 x2 x3 x4) pat) Hclose.
diff --git a/theories/base_logic/lib/na_invariants.v b/theories/base_logic/lib/na_invariants.v
index 08470051f88b13fb08f0e93aeed2129d353a0ad1..6b5296060ad86699555071a1c2e9a9ebb643165f 100644
--- a/theories/base_logic/lib/na_invariants.v
+++ b/theories/base_logic/lib/na_invariants.v
@@ -110,4 +110,16 @@ Section proofs.
       + iFrame. iApply "Hclose". iNext. iLeft. by iFrame.
     - iDestruct (na_own_disjoint with "Htoki Htoki2") as %?. set_solver.
   Qed.
+
+  Global Instance into_inv_na p N P : IntoInv (na_inv p N P) N.
+  Global Instance elim_inv_na p F E N P Q Q':
+    (∀ R, ElimModal True (|={E}=> R)%I R Q Q') →
+    ElimInv (↑N ⊆ E ∧ ↑N ⊆ F) (na_inv p N P) (na_own p F)
+      (▷ P ∗ na_own p (F∖↑N)) (▷ P ∗ na_own p (F∖↑N) ={E}=∗ na_own p F) Q Q'.
+  Proof.
+    rewrite /ElimInv /ElimModal. iIntros (Helim (?&?)) "(#H1&Hown&H2)".
+    iApply (Helim with "[- $H2]"); first done.
+    iMod (na_inv_open p E F N P with "[#] [Hown]") as "(HP&Hown&Hclose)"; auto. 
+    by iFrame.
+  Qed.
 End proofs.
diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index 511c267bfaaf3ede91e8db55c384da6efee4c1be..1c216f2bcf6a28a7b279af66bbca4d7fcb28210b 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -394,7 +394,7 @@ Canonical Structure monPredSI : sbi :=
 End canonical_sbi.
 
 Class Absolute {I : biIndex} {PROP : bi} (P : monPred I PROP) :=
-  absolute_at V1 V2 : P V1 -∗ P V2.
+  absolute_at i j : P i -∗ P j.
 Arguments Absolute {_ _} _%I.
 Arguments absolute_at {_ _} _%I {_}.
 Hint Mode Absolute + + ! : typeclass_instances.
@@ -452,11 +452,11 @@ Proof. move => [] /(_ i). unfold Affine. by unseal. Qed.
 
 (* Note that monPred_in is *not* Plain, because it does depend on the
    index. *)
-Global Instance monPred_in_persistent V :
-  Persistent (@monPred_in I PROP V).
+Global Instance monPred_in_persistent i :
+  Persistent (@monPred_in I PROP i).
 Proof. unfold Persistent. unseal; split => ?. by apply bi.pure_persistent. Qed.
-Global Instance monPred_in_absorbing V :
-  Absorbing (@monPred_in I PROP V).
+Global Instance monPred_in_absorbing i :
+  Absorbing (@monPred_in I PROP i).
 Proof. unfold Absorbing. unseal. split=> ? /=. apply absorbing, _. Qed.
 
 
@@ -657,35 +657,35 @@ Global Instance relatively_absolute P : Absolute (∃ᵢ P).
 Proof. apply emb_absolute. Qed.
 
 Global Instance and_absolute P Q `{!Absolute P, !Absolute Q} : Absolute (P ∧ Q).
-Proof. intros ??. unseal. by rewrite !(absolute_at _ V1 V2). Qed.
+Proof. intros i j. unseal. by rewrite !(absolute_at _ i j). Qed.
 Global Instance or_absolute P Q `{!Absolute P, !Absolute Q} : Absolute (P ∨ Q).
-Proof. intros ??. by rewrite !monPred_at_or !(absolute_at _ V1 V2). Qed.
+Proof. intros i j. by rewrite !monPred_at_or !(absolute_at _ i j). Qed.
 Global Instance impl_absolute P Q `{!Absolute P, !Absolute Q} : Absolute (P → Q).
 Proof.
-  intros ??. unseal. rewrite (bi.forall_elim V1) bi.pure_impl_forall.
-  rewrite bi.forall_elim //. apply bi.forall_intro=>V'.
+  intros i j. unseal. rewrite (bi.forall_elim i) bi.pure_impl_forall.
+  rewrite bi.forall_elim //. apply bi.forall_intro=> k.
   rewrite bi.pure_impl_forall. apply bi.forall_intro=>_.
-  rewrite (absolute_at Q V1). by rewrite (absolute_at P V').
+  rewrite (absolute_at Q i). by rewrite (absolute_at P k).
 Qed.
 Global Instance forall_absolute {A} Φ {H : ∀ x : A, Absolute (Φ x)} :
   @Absolute I PROP (∀ x, Φ x)%I.
-Proof. intros ??. unseal. do 2 f_equiv. by apply absolute_at. Qed.
+Proof. intros i j. unseal. do 2 f_equiv. by apply absolute_at. Qed.
 Global Instance exists_absolute {A} Φ {H : ∀ x : A, Absolute (Φ x)} :
   @Absolute I PROP (∃ x, Φ x)%I.
-Proof. intros ??. unseal. do 2 f_equiv. by apply absolute_at. Qed.
+Proof. intros i j. unseal. do 2 f_equiv. by apply absolute_at. Qed.
 
 Global Instance sep_absolute P Q `{!Absolute P, !Absolute Q} : Absolute (P ∗ Q).
-Proof. intros ??. unseal. by rewrite !(absolute_at _ V1 V2). Qed.
+Proof. intros i j. unseal. by rewrite !(absolute_at _ i j). Qed.
 Global Instance wand_absolute P Q `{!Absolute P, !Absolute Q} : Absolute (P -∗ Q).
 Proof.
-  intros ??. unseal. rewrite (bi.forall_elim V1) bi.pure_impl_forall.
-  rewrite bi.forall_elim //. apply bi.forall_intro=>V'.
+  intros i j. unseal. rewrite (bi.forall_elim i) bi.pure_impl_forall.
+  rewrite bi.forall_elim //. apply bi.forall_intro=> k.
   rewrite bi.pure_impl_forall. apply bi.forall_intro=>_.
-  rewrite (absolute_at Q V1). by rewrite (absolute_at P V').
+  rewrite (absolute_at Q i). by rewrite (absolute_at P k).
 Qed.
 Global Instance persistently_absolute P `{!Absolute P} :
   Absolute (bi_persistently P).
-Proof. intros ??. unseal. by rewrite absolute_at. Qed.
+Proof. intros i j. unseal. by rewrite absolute_at. Qed.
 
 Global Instance affinely_absolute P `{!Absolute P} : Absolute (bi_affinely P).
 Proof. rewrite /bi_affinely. apply _. Qed.
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index edca5f5e9e20031c34be87b75b16d12ec9de64be..0bd44bb9702f3231ab5e50551cbab073ff58035e 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -1,4 +1,5 @@
 From iris.bi Require Export bi.
+From stdpp Require Import namespaces.
 Set Default Proof Using "Type".
 Import bi.
 
@@ -478,6 +479,32 @@ Proof. by apply as_valid. Qed.
 Lemma as_valid_2 (φ : Prop) {PROP : bi} (P : PROP) `{!AsValid φ P} : P → φ.
 Proof. by apply as_valid. Qed.
 
+(* Input: [P]; Outputs: [N],
+   Extracts the namespace associated with an invariant assertion. Used for [iInv]. *)
+Class IntoInv {PROP : bi} (P: PROP) (N: namespace).
+Arguments IntoInv {_} _%I _.
+Hint Mode IntoInv + ! - : typeclass_instances.
+
+(* Input: [Pinv]
+   Arguments:
+   - [Pinv] is an invariant assertion
+   - [Pin] is an additional assertion needed for opening an invariant
+   - [Pout] is the assertion obtained by opening the invariant
+   - [Pclose] is the assertion which contains an update modality to close the invariant
+   - [Q] is a goal on which iInv may be invoked
+   - [Q'] is the transformed goal that must be proved after opening the invariant.
+
+   There are similarities to the definition of ElimModal, however we
+   want to be general enough to support uses in settings where there
+   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) (Pinv Pin Pout Pclose Q Q' : PROP) :=
+  elim_inv : φ → Pinv ∗ Pin ∗ (Pout ∗ Pclose -∗ Q') ⊢ Q.
+Arguments ElimInv {_} _ _ _%I _%I _%I _%I : simpl never.
+Arguments elim_inv {_} _ _ _%I _%I _%I _%I _%I _%I.
+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
 definitions opaque for type class search. For example, when using `iDestruct`,
@@ -523,3 +550,8 @@ Instance from_modal_tc_opaque {PROP : bi} (P Q : PROP) :
   FromModal P Q → FromModal (tc_opaque P) Q := id.
 Instance elim_modal_tc_opaque {PROP : bi} φ (P P' Q Q' : PROP) :
   ElimModal φ P P' Q Q' → ElimModal φ (tc_opaque P) P' Q Q' := id.
+Instance into_inv_tc_opaque {PROP : bi} (P : PROP) N :
+  IntoInv P N → IntoInv (tc_opaque P) N := id.
+Instance elim_inv_tc_opaque {PROP : bi} φ (Pinv Pin Pout Pclose Q Q' : PROP) :
+  ElimInv φ Pinv Pin Pout Pclose Q Q' →
+  ElimInv φ (tc_opaque Pinv) Pin Pout Pclose Q Q' := id.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 33c0287b721cc75bc8f38bfe3dc75915af4d2f5b..840d129b0194424968ca9e44f40b46e103e5d48d 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -209,6 +209,16 @@ Proof.
   repeat apply sep_mono=>//; apply affinely_persistently_if_flag_mono; by destruct q1.
 Qed.
 
+Lemma envs_lookup_delete_list_cons Δ Δ' Δ'' rp j js p1 p2 P Ps :
+  envs_lookup_delete rp j Δ = Some (p1, P, Δ') →
+  envs_lookup_delete_list rp js Δ' = Some (p2, Ps, Δ'') →
+  envs_lookup_delete_list rp (j :: js) Δ = Some (p1 && p2, (P :: Ps), Δ'').
+Proof. rewrite //= => -> //= -> //=. Qed.
+
+Lemma envs_lookup_delete_list_nil Δ rp :
+  envs_lookup_delete_list rp [] Δ = Some (true, [], Δ).
+Proof. done. Qed.
+
 Lemma envs_lookup_snoc Δ i p P :
   envs_lookup i Δ = None → envs_lookup i (envs_snoc Δ p i P) = Some (p, P).
 Proof.
@@ -1159,6 +1169,22 @@ Proof.
   rewrite envs_entails_eq => ???? HΔ. rewrite envs_replace_singleton_sound //=.
   rewrite HΔ affinely_persistently_if_elim. by eapply elim_modal.
 Qed.
+
+(** * Invariants *)
+Lemma tac_inv_elim Δ Δ' i j φ p P Pin Pout Pclose Q Q' :
+  envs_lookup_delete false i Δ = Some (p, P, Δ') →
+  ElimInv φ P Pin Pout Pclose Q Q' →
+  φ →
+  (∀ R, ∃ Δ'',
+    envs_app false (Esnoc Enil j (Pin -∗ (Pout -∗ Pclose -∗ Q') -∗ R)%I) Δ' = Some Δ'' ∧
+    envs_entails Δ'' R) →
+  envs_entails Δ Q.
+Proof.
+  rewrite envs_entails_eq=> /envs_lookup_delete_Some [? ->] ?? /(_ Q) [Δ'' [? <-]].
+  rewrite (envs_lookup_sound' _ false) // envs_app_singleton_sound //; simpl.
+  apply wand_elim_r', wand_mono; last done. apply wand_intro_r, wand_intro_r.
+  rewrite affinely_persistently_if_elim -assoc wand_curry. auto.
+Qed.
 End bi_tactics.
 
 Section sbi_tactics.
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 458b507562e024891a37636d3139d4081957dd68..2fd6728b5b85ffbb444c724d9d09b5f62ffbcf38 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -1,6 +1,7 @@
 From iris.proofmode Require Import coq_tactics.
 From iris.proofmode Require Import base intro_patterns spec_patterns sel_patterns.
 From iris.bi Require Export bi big_op.
+From stdpp Require Import namespaces.
 From iris.proofmode Require Export classes notation.
 From iris.proofmode Require Import class_instances.
 From stdpp Require Import hlist pretty.
@@ -1864,6 +1865,92 @@ 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).
 
+(** * Invariant *)
+
+(* Finds a hypothesis in the context that is an invariant with
+   namespace [N].  To do so, we check whether for each hypothesis
+   ["H":P] we can find an instance of [IntoInv P N] *)
+Tactic Notation "iAssumptionInv" constr(N) :=
+  let rec find Γ i :=
+    lazymatch Γ with
+    | Esnoc ?Γ ?j ?P' =>
+      first [let H := constr:(_: IntoInv P' N) in unify i j|find Γ i]
+    end in
+  lazymatch goal with
+  | |- envs_lookup_delete _ ?i (Envs ?Γp ?Γs) = Some _ =>
+     first [find Γp i|find Γs i]; env_reflexivity
+  end.
+
+(* 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
+  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 (
+       iApplyHyp H; clear R;
+       iIntros H; (* H was spatial, so it's gone due to the apply and we can reuse the name *)
+       iIntros Hclose;
+       tac H
+    )].
+
+Tactic Notation "iInvCore" constr(N) "as" tactic(tac) constr(Hclose) :=
+  iInvCore N with "[$]" as ltac:(tac) Hclose.
+
+Tactic Notation "iInv" constr(N) "as" constr(pat) constr(Hclose) :=
+   iInvCore N as (fun H => iDestructHyp H as pat) Hclose.
+Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1) ")"
+    constr(pat) constr(Hclose) :=
+   iInvCore N as (fun H => iDestructHyp H as (x1) pat) Hclose.
+Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) ")" constr(pat) constr(Hclose) :=
+   iInvCore N as (fun H => iDestructHyp H as (x1 x2) pat) Hclose.
+Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) ")"
+    constr(pat) constr(Hclose) :=
+   iInvCore N as (fun H => iDestructHyp H as (x1 x2 x3) pat) Hclose.
+Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
+    constr(pat) constr(Hclose) :=
+   iInvCore N as (fun H => iDestructHyp H as (x1 x2 x3 x4) pat) Hclose.
+Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" constr(pat) constr(Hclose) :=
+   iInvCore N with Hs as (fun H => iDestructHyp H as pat) Hclose.
+Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(x1) ")"
+    constr(pat) constr(Hclose) :=
+   iInvCore N with Hs as (fun H => iDestructHyp H as (x1) pat) Hclose.
+Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) ")" constr(pat) constr(Hclose) :=
+   iInvCore N with Hs as (fun H => iDestructHyp H as (x1 x2) pat) Hclose.
+Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) ")"
+    constr(pat) constr(Hclose) :=
+   iInvCore N with Hs as (fun H => iDestructHyp H as (x1 x2 x3) pat) Hclose.
+Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
+    constr(pat) constr(Hclose) :=
+   iInvCore N with Hs as (fun H => iDestructHyp H as (x1 x2 x3 x4) pat) Hclose.
+
 Hint Extern 0 (_ ⊢ _) => iStartProof.
 
 (* Make sure that by and done solve trivial things in proof mode *)
diff --git a/theories/tests/proofmode_iris.v b/theories/tests/proofmode_iris.v
index f22e3838ee11d88973c94d78cc60d124ee9878f4..b702dd7450c75c73088f78016d31c5f77b2b3677 100644
--- a/theories/tests/proofmode_iris.v
+++ b/theories/tests/proofmode_iris.v
@@ -1,5 +1,6 @@
 From iris.proofmode Require Import tactics.
-From iris.base_logic Require Import base_logic lib.invariants.
+From iris.base_logic Require Import base_logic.
+From iris.base_logic.lib Require Import invariants cancelable_invariants na_invariants.
 
 Section base_logic_tests.
   Context {M : ucmraT}.
@@ -48,7 +49,7 @@ Section base_logic_tests.
 End base_logic_tests.
 
 Section iris_tests.
-  Context `{invG Σ}.
+  Context `{invG Σ, cinvG Σ, na_invG Σ}.
 
   Lemma test_masks  N E P Q R :
     ↑N ⊆ E →
@@ -58,4 +59,152 @@ Section iris_tests.
     iApply ("H" with "[% //] [$] [> HQ] [> //]").
     by iApply inv_alloc.
   Qed.
+
+  Lemma test_iInv_0 N P: inv N (bi_persistently P) ={⊤}=∗ ▷ P.
+  Proof.
+    iIntros "#H".
+    iInv N as "#H2" "Hclose".
+    iMod ("Hclose" with "H2").
+    iModIntro. by iNext.
+  Qed.
+
+  Lemma test_iInv_1 N E P:
+    ↑N ⊆ E →
+    inv N (bi_persistently P) ={E}=∗ ▷ P.
+  Proof.
+    iIntros (?) "#H".
+    iInv N as "#H2" "Hclose".
+    iMod ("Hclose" with "H2").
+    iModIntro. by iNext.
+  Qed.
+
+  Lemma test_iInv_2 γ p N P:
+    cinv N γ (bi_persistently P) ∗ cinv_own γ p ={⊤}=∗ cinv_own γ p ∗ ▷ P.
+  Proof.
+    iIntros "(#?&?)".
+    iInv N as "(#HP&Hown)" "Hclose".
+    iMod ("Hclose" with "HP").
+    iModIntro. iFrame. by iNext.
+  Qed.
+
+  Lemma test_iInv_3 γ p1 p2 N P:
+    cinv N γ (bi_persistently P) ∗ cinv_own γ p1 ∗ cinv_own γ p2
+      ={⊤}=∗ cinv_own γ p1 ∗ cinv_own γ p2  ∗ ▷ P.
+  Proof.
+    iIntros "(#?&Hown1&Hown2)".
+    iInv N with "[Hown2 //]" as "(#HP&Hown2)" "Hclose".
+    iMod ("Hclose" with "HP").
+    iModIntro. iFrame. by iNext.
+  Qed.
+
+  Lemma test_iInv_4 t N E1 E2 P:
+    ↑N ⊆ E2 →
+    na_inv t N (bi_persistently P) ∗ na_own t E1 ∗ na_own t E2
+         ⊢ |={⊤}=> na_own t E1 ∗ na_own t E2  ∗ ▷ P.
+  Proof.
+    iIntros (?) "(#?&Hown1&Hown2)".
+    iInv N as "(#HP&Hown2)" "Hclose".
+    iMod ("Hclose" with "[HP Hown2]").
+    { iFrame. done. }
+    iModIntro. iFrame. by iNext.
+  Qed.
+
+  (* test named selection of which na_own to use *)
+  Lemma test_iInv_5 t N E1 E2 P:
+    ↑N ⊆ E2 →
+    na_inv t N (bi_persistently P) ∗ na_own t E1 ∗ na_own t E2
+      ={⊤}=∗ na_own t E1 ∗ na_own t E2  ∗ ▷ P.
+  Proof.
+    iIntros (?) "(#?&Hown1&Hown2)".
+    iInv N with "Hown2" as "(#HP&Hown2)" "Hclose".
+    iMod ("Hclose" with "[HP Hown2]").
+    { iFrame. done. }
+    iModIntro. iFrame. by iNext.
+  Qed.
+
+  Lemma test_iInv_6 t N E1 E2 P:
+    ↑N ⊆ E1 →
+    na_inv t N (bi_persistently P) ∗ na_own t E1 ∗ na_own t E2
+      ={⊤}=∗ na_own t E1 ∗ na_own t E2  ∗ ▷ P.
+  Proof.
+    iIntros (?) "(#?&Hown1&Hown2)".
+    iInv N with "Hown1" as "(#HP&Hown1)" "Hclose".
+    iMod ("Hclose" with "[HP Hown1]").
+    { iFrame. done. }
+    iModIntro. iFrame. by iNext.
+  Qed.
+
+  (* test robustness in presence of other invariants *)
+  Lemma test_iInv_7 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 (?) "(#?&#?&#?&Hown1&Hown2)".
+    iInv N3 with "Hown1" as "(#HP&Hown1)" "Hclose".
+    iMod ("Hclose" with "[HP Hown1]").
+    { iFrame. done. }
+    iModIntro. iFrame. by iNext.
+  Qed.
+
+  (* iInv should work even where we have "inv N P" in which P contains an evar *)
+  Lemma test_iInv_8 N : ∃ P, inv N P ={⊤}=∗ P ≡ True ∧ inv N P.
+  Proof.
+    eexists. iIntros "#H".
+    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.
+
+  (* test destruction of existentials when opening an invariant *)
+  Lemma test_iInv_13 N:
+    inv N (∃ (v1 v2 v3 : nat), emp ∗ emp ∗ emp) ={⊤}=∗ ▷ emp.
+  Proof.
+    iIntros "H"; iInv "H" as (v1 v2 v3) "(?&?&_)" "Hclose".
+    iMod ("Hclose" with "[]").
+    { iNext; iExists O; done. }
+    iModIntro. by iNext.
+  Qed.
 End iris_tests.