From ad0201e9f3ba2fe4180ca3c400f8ea5648d970ca Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 30 May 2018 13:54:54 +0200
Subject: [PATCH] Fix typo in ProofMode.md (thanks to Hai).

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

diff --git a/ProofMode.md b/ProofMode.md
index 06ba8e1c8..4911c0c69 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -41,8 +41,8 @@ Context management
   the resulting goal.
 - `iPoseProof pm_trm as (x1 ... xn) "ipat"` : put `pm_trm` into the context and
   eliminates it. This tactic is essentially the same as `iDestruct` with the
-  difference that when `pm_trm` is a non-univerisally quantified spatial
-  hypothesis, it will not throw the hypothesis away.
+  difference that when `pm_trm` is a non-univerisally quantified persistent
+  hypothesis, it will not throw away the hypothesis.
 - `iAssert P with "spat" as "ipat"` : generates a new subgoal `P` and adds the
   hypothesis `P` to the current goal. The specialization pattern `spat`
   specifies which hypotheses will be consumed by proving `P`. The introduction
-- 
GitLab