From b2e7e52fea7635221ff0fd7602a32ce3b2b9b7a3 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 10 Dec 2017 14:18:17 +0100
Subject: [PATCH] Docs: fix typo.

---
 docs/program-logic.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/docs/program-logic.tex b/docs/program-logic.tex
index a009324a9..06a9f7495 100644
--- a/docs/program-logic.tex
+++ b/docs/program-logic.tex
@@ -367,7 +367,7 @@ The adequacy statement now reads as follows:
 Notice that the state invariant $S$ used by the weakest precondition is chosen \emph{after} doing a fancy update, which allows it to depend on the names of ghost variables that are picked in that initial fancy update.
 
 \paragraph{Hoare triples.}
-It turns out that weakest precondition is actually quite convenient to work with, in particular when perfoming these proofs in Coq.
+It turns out that weakest precondition is actually quite convenient to work with, in particular when performing these proofs in Coq.
 Still, for a more traditional presentation, we can easily derive the notion of a Hoare triple:
 \[
 \hoare{\prop}{\expr}{\Ret\val.\propB}[\mask] \eqdef \always{(\prop \wand \wpre{\expr}[\mask]{\Ret\val.\propB})}
-- 
GitLab