diff --git a/README.md b/README.md
index 48b24f1530788c72f6dc8a0ed68ab152819ffa39..39ff167a06809785b7c1950d5596db1aaae3a2b4 100644
--- a/README.md
+++ b/README.md
@@ -1,7 +1,6 @@
-# IRIS COQ DEVELOPMENT, MOSEL VERSION
+# IRIS COQ DEVELOPMENT
 
-This is the Coq development of the [Iris Project](http://iris-project.org), in
-the MoSeL version.
+This is the Coq development of the [Iris Project](http://iris-project.org).
 
 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