From 9acbe81f7670e8e86acb35afe286afa3fb0e19a0 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 18 Oct 2019 09:43:07 +0200
Subject: [PATCH] More README tweaks.

---
 README.md | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/README.md b/README.md
index 6ccb5cb..e96e620 100644
--- a/README.md
+++ b/README.md
@@ -111,6 +111,10 @@ mechanization in Coq:
 There are a number of small differences between the paper presentation
 of Actris and the formalization in Coq, that are briefly discussed here.
 
+- **Weakest preconditions versus Hoare triples**
+
+  See the section "Weakest preconditions and Coq tactics" above.
+  
 - **Connectives for physical ownership of channels**
 
   In the paper, physical ownership of a channel is formalized using a single
@@ -123,6 +127,7 @@ of Actris and the formalization in Coq, that are briefly discussed here.
   intuitive but gives rise to a more practical Jacobs/Piessens-style spec of
   `recv` that does not need a closing view shift (to handle the case that the
   buffer is empty).
+
 - **Later modalities in primitive rules for channels**
 
   The primitive rules for `send` and `recv` (`send_spec` and `recv_spec` in
-- 
GitLab