From a7b8df6f685d13e774f615eb5e9a479b19c53c04 Mon Sep 17 00:00:00 2001
From: Joseph Tassarotti <jtassaro@andrew.cmu.edu>
Date: Tue, 20 Feb 2018 09:37:32 -0500
Subject: [PATCH] More comments about iInv tactics.

---
 ProofMode.md                 |  7 +++++--
 theories/proofmode/classes.v | 17 +++++++++--------
 theories/proofmode/tactics.v |  5 +++++
 3 files changed, 19 insertions(+), 10 deletions(-)

diff --git a/ProofMode.md b/ProofMode.md
index 02aabe071..845d81fd3 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 f0f070278..3d1bb6a87 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 5108a40a4..59945b400 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
-- 
GitLab