diff --git a/ProofMode.md b/ProofMode.md
index 02aabe071b0533e754b3e7a0fd38a24305b6da21..845d81fd334dad13799e6327ba2a05c32d1e114c 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 (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`.
Miscellaneous
-------------
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index f0f07027851a3967add874ea7254ef157719e9af..3d1bb6a87fd80d74b5b43dbc36e6311c57e0679f 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -468,18 +468,19 @@ 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`. *)
+(* 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`;
- - `Pinv`, an invariant assertion
- - `Pin` the additional assertions needed for opening an invariant;
- - `Pout` is the assertion obtained by opening 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.
+(* 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
+ - [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
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 5108a40a4029ef08237c6d02cbbb778524ed0796..59945b400d9f4166b631ce63d65adcde1727f3b0 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -1865,6 +1865,11 @@ 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 *)
+
+(* 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 P :=
lazymatch Γ with