From 02513979b13521909927d4e760e6a4e3e05d2178 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 24 Jan 2019 13:48:08 +0100
Subject: [PATCH] tweaks

---
 CONTRIBUTING.md |  7 -------
 README.md       | 10 ++++++++--
 2 files changed, 8 insertions(+), 9 deletions(-)

diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 581b6534e..f7d8805be 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -9,13 +9,6 @@ tab).  If you want to report a bug, please use the
 [issue tracker](https://gitlab.mpi-sws.org/FP/iris-coq/issues), which also
 requires an MPI-SWS GitLab account.
 
-Below, you can find some useful resources and an FAQ.
-
-* Information on how to set up your editor for unicode input and output is
-  collected in [Editor.md](Editor.md).
-* The Iris Proof Mode (IPM) / MoSeL is documented at [ProofMode.md](ProofMode.md).
-* Naming conventions are documented at [Naming.md](Naming.md).
-
 ## How to submit a merge request
 
 To contribute code, please send your MPI-SWS GitLab username to
diff --git a/README.md b/README.md
index a08ef686d..e99525d73 100644
--- a/README.md
+++ b/README.md
@@ -108,6 +108,12 @@ that should be compatible with this version:
 * [Iris Atomic](https://gitlab.mpi-sws.org/FP/iris-atomic/) is an experimental
   formalization of logically atomic triples in Iris.
 
-## Notes for Iris Contributors
+## Notes for Iris Developers
 
-See the [contribution guide](CONTRIBUTING.md).
+* Information on how to set up your editor for unicode input and output is
+  collected in [Editor.md](Editor.md).
+* The Iris Proof Mode (IPM) / MoSeL is documented at [ProofMode.md](ProofMode.md).
+* Naming conventions are documented at [Naming.md](Naming.md).
+* The generated coqdoc is [available online](https://plv.mpi-sws.org/coqdoc/iris/).
+
+To contribute to Iris itself, see the [contribution guide](CONTRIBUTING.md).
-- 
GitLab