From 989c871aa14b9280326d3898be9987772085ad47 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 24 Jul 2018 22:11:09 +0200
Subject: [PATCH] Update README.md even more

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

diff --git a/README.md b/README.md
index e47c07595..a96743610 100644
--- a/README.md
+++ b/README.md
@@ -1,7 +1,8 @@
 # IRIS COQ DEVELOPMENT
 
 This is the Coq development of the [Iris Project](http://iris-project.org),
-which includes the [MoSeL proof mode](http://iris-project.org/mosel/).
+which includes [MoSeL](http://iris-project.org/mosel/), a general proof mode
+for carrying out separation logic proofs in Coq.
 
 A LaTeX version of the core logic definitions and some derived forms is
 available in [docs/iris.tex](docs/iris.tex).  A compiled PDF version of this
-- 
GitLab