diff --git a/README.md b/README.md
index 7b3d055196f02031bc6881141fae80747ca94e16..e47c075951e3413c2d142bba147db5af37ccfda0 100644
--- a/README.md
+++ b/README.md
@@ -1,6 +1,7 @@
 # IRIS COQ DEVELOPMENT
 
-This is the Coq development of the [Iris Project](http://iris-project.org).
+This is the Coq development of the [Iris Project](http://iris-project.org),
+which includes the [MoSeL proof mode](http://iris-project.org/mosel/).
 
 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