From d5ff27dc22c4a9fe766ef0f7afb3bd8e95aaf6d9 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 17 Mar 2016 17:20:31 +0100
Subject: [PATCH] more links in README

---
 README.md | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

diff --git a/README.md b/README.md
index ffc56661e..6e160a662 100644
--- a/README.md
+++ b/README.md
@@ -1,4 +1,8 @@
-# PREREQUISITES
+# IRIS COQ DEVELOPMENT
+
+This is the Coq development of the [Iris Project](http://plv.mpi-sws.org/iris/).
+
+## Prerequisites
 
 This version is known to compile with:
 
@@ -11,7 +15,7 @@ fetch the development branch yourself). Iris compiles fine even without this
 patch, but proof bullets will only be in 'strict' (enforcing) mode with the
 fixed version of Ssreflect.
  
-# BUILDING INSTRUCTIONS
+## Building Instructions
 
 Run the following command to build the full development:
 
@@ -22,7 +26,7 @@ running:
 
     make install
 
-# STRUCTURE
+## Structure
 
 * The folder `prelude` contains an extended "Standard Library" by Robbert
   Krebbers <http://robbertkrebbers.nl/thesis.html>.
@@ -36,7 +40,7 @@ running:
 * The folder `barrier` contains the implementation and proof of the barrier
   <http://doi.acm.org/10.1145/2818638>.
 
-# DOCUMENTATION
+## Documentation
 
 A LaTeX version of the core logic definitions and some derived forms is
 available in `docs/iris.tex`.
-- 
GitLab