From 4cf90c36c2d418ab30c42e47bce866a7f6aa35dc Mon Sep 17 00:00:00 2001
From: Ralf Jung
Date: Tue, 15 Mar 2016 23:15:04 +0100
Subject: [PATCH] markdown README

README  20 
README.md  33 +++++++++++++++++++++++++++++++++
program_logic/weakestpre.v  2 +
3 files changed, 34 insertions(+), 21 deletions()
delete mode 100644 README
create mode 100644 README.md
diff git a/README b/README
deleted file mode 100644
index e1e61a2c..00000000
 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 00000000..41e3afbe
 /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 023a801a..85fc236c 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 Φ Ψ :

2.26.2