diff git a/README b/README
deleted file mode 100644
index e1e61a2c4ec948625d648435feebbe2fd7612463..0000000000000000000000000000000000000000
 a/README
+++ /dev/null
@@ 1,20 +0,0 @@
PREREQUISITES


This version is known to compile with:

  Coq 8.5
  Ssreflect 1.6

For development, better make sure you have a version of Ssreflect that includes
commit be724937 (no such version has been released so far, you will have to
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


Run the following command to build the full development:

 make
diff git a/README.md b/README.md
new file mode 100644
index 0000000000000000000000000000000000000000..41e3afbef0234f3cdf07158bee3150a1adfc9e07
 /dev/null
+++ b/README.md
@@ 0,0 +1,33 @@
+# PREREQUISITES
+
+This version is known to compile with:
+
+  Coq 8.5
+  Ssreflect 1.6
+
+For development, better make sure you have a version of Ssreflect that includes
+commit be724937 (no such version has been released so far, you will have to
+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
+
+Run the following command to build the full development:
+
+ make
+
+
+# STRUCTURE
+
+* The folder `prelude` contains an extended "Standard Library" by Robbert
+ Krebbers .
+* The folder `algebra` contains the COFE and CMRA constructions as well as
+ the solver for recursive domain equations.
+* The folder `program_logic` builds the semantic domain of Iris, defines and
+ verifies primitive view shifts and weakest preconditions, and builds some
+ languageindependent derived constructions (e.g., STSs).
+* The folder `heap_lang` defines the MLlike concurrent heap language, and a
+ few derived constructions (e.g., parallel composition).
+* The folder `barrier` contains the implementation and proof of the barrier.
+* The folder `examples` contains the examples given in the paper.
diff git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index 023a801aaa6058ea1a20e173000bcbabd2e53fff..85fc236c54485e7bde79d8c90991fdfa592b2c9b 100644
 a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ 248,7 +248,7 @@ Proof. by setoid_rewrite (always_and_sep_r _ _); rewrite wp_frame_r. Qed.
Lemma wp_impl_l E e Φ Ψ :
((□ ∀ v, Φ v → Ψ v) ∧ WP e @ E {{ Φ }}) ⊢ WP e @ E {{ Ψ }}.
Proof.
 rewrite wp_always_l; apply wp_mono=> // v.
+ rewrite wp_always_l. apply wp_mono=> // v.
by rewrite always_elim (forall_elim v) impl_elim_l.
Qed.
Lemma wp_impl_r E e Φ Ψ :