From 9064e78f4f5677db7192e7e04fb0698173872562 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 9 Jul 2018 12:58:36 +0200
Subject: [PATCH] README: add link to MoSeL paper website

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

diff --git a/README.md b/README.md
index 39ff167a0..2aaedbe39 100644
--- a/README.md
+++ b/README.md
@@ -73,9 +73,10 @@ followed by `make build-dep`.
   constructions that work for any such language.
 * The folder [bi](theories/bi) contains the BI++ laws, as well as derived
   connectives, laws and constructions that are applicable for general BIS.
-* The folder [proofmode](theories/proofmode) contains MoSeL, which extends Coq
-  with contexts for intuitionistic and spatial BI++ assertions. It also contains
-  tactics for interactive proofs. Documentation can be found in
+* The folder [proofmode](theories/proofmode) contains
+  [MoSeL](http://iris-project.org/mosel/), which extends Coq with contexts for
+  intuitionistic and spatial BI++ assertions. It also contains tactics for
+  interactive proofs. Documentation can be found in
   [ProofMode.md](ProofMode.md).
 * The folder [heap_lang](theories/heap_lang) defines the ML-like concurrent heap
   language
-- 
GitLab