From c5bcacc061e6438e225f1ef4d0f43f17f9e4ed7f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 30 Nov 2018 10:38:52 +0100
Subject: [PATCH] change how we link to coqdoc

---
 README.md | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

diff --git a/README.md b/README.md
index 40ebf197f..c4fcf9e2e 100644
--- a/README.md
+++ b/README.md
@@ -1,14 +1,16 @@
-# IRIS COQ DEVELOPMENT
+# IRIS COQ DEVELOPMENT [[coqdoc]](https://plv.mpi-sws.org/coqdoc/iris/)
 
 This is the Coq development of the [Iris Project](http://iris-project.org),
 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
-document is [available online](http://plv.mpi-sws.org/iris/appendix-3.1.pdf).
-An HTML version of the latest sources (with hyperlinks for easier navigation) is
-available at https://plv.mpi-sws.org/coqdoc/iris/.
+For using the Coq library, check out the
+[API documentation](https://plv.mpi-sws.org/coqdoc/iris/).
+
+For understanding the theory of Iris, 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 document is
+[available online](http://plv.mpi-sws.org/iris/appendix-3.1.pdf).
 
 ## Building Iris
 
-- 
GitLab