From 50d85ae3b569c2f38bbb36eb8c8447b81e56438b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 19 Feb 2018 19:41:36 +0100
Subject: [PATCH] Fix typo.

---
 ProofMode.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/ProofMode.md b/ProofMode.md
index cc19fdf3d..dc14b03b6 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -41,7 +41,7 @@ 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
+  difference that when `pm_trm` is a non-universally quantified spatial
   hypothesis, it will not throw the hypothesis away.
 - `iAssert P with "spat" as "ipat"` : generates a new subgoal `P` and adds the
   hypothesis `P` to the current goal. The specialization pattern `spat`
-- 
GitLab