From d62f14ed739a93cf1e829170efe0bd765719bb6d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 1 May 2019 19:12:27 +0200
Subject: [PATCH] Markdown nits in ProofMode.md
---
ProofMode.md | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/ProofMode.md b/ProofMode.md
index 529ede69d..fe780136f 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`.
--
GitLab