From 3f7f9f4e0cb404aa5936255288fa8e15a3be12b6 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 23 Apr 2019 16:20:25 +0200
Subject: [PATCH] Update example in ProofMode.md

---
 ProofMode.md | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/ProofMode.md b/ProofMode.md
index 9d2220a73..4e8a15993 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -237,11 +237,13 @@ appear at the top level:
 
 For example, given:
 
-        ∀ x, x = 0 ⊢ □ (P → False ∨ □ (Q ∧ ▷ R) -∗ P ∗ ▷ (R ∗ Q ∧ x = pred 2)).
+        ∀ x, <affine> ⌜ x = 0 ⌝ ⊢
+          □ (P → False ∨ □ (Q ∧ ▷ R) -∗
+          P ∗ ▷ (R ∗ Q ∧ ⌜ x = pred 2 ⌝)).
 
 You can write
 
-        iIntros (x) "% !# $ [[] | #[HQ HR]] /= !>".
+        iIntros (x Hx) "!# $ [[] | #[HQ HR]] /= !>".
 
 which results in:
 
-- 
GitLab