diff --git a/ProofMode.md b/ProofMode.md
index 529ede69dfa410631ad69671539d513f903fa32f..fe780136f36988dbdc816151ea1ec8d884517dc4 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -171,8 +171,8 @@ Iris
 ----
 
 - `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
+   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`.