From 4664362819967578f51e0ef08b1735940bb288f2 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 13 Apr 2016 00:49:08 +0200
Subject: [PATCH] Update README.

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

diff --git a/README.md b/README.md
index 4b73aab77..3db43d58e 100644
--- a/README.md
+++ b/README.md
@@ -40,6 +40,9 @@ running:
     language, e.g., parallel composition.
     Most notable here s `lib/barrier`, the implementation and proof of a barrier
     as described in <http://doi.acm.org/10.1145/2818638>.
+* The folder `proofmode` contains the Iris proof mode, which extends Coq with
+  contexts for persistent and spatial Iris assertions. It also contains tactics
+  for interactive proofs in Iris.
 * The folder `tests` contains modules we use to test our infrastructure.
   Users of the Iris Coq library should *not* depend on these modules; they may
   change or disappear without any notice.
-- 
GitLab