From b7401c6873df5454b328901686565beb88ac7341 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 3 Feb 2016 16:51:48 +0100
Subject: [PATCH] Revert "Remove FIXME now that ssr bug #22 is fixed."

We should not depend on unreleased, git-only versions.
This reverts commit ee9480281f8a30273b66c1e195b9e546014a61b8.
---
 README              | 8 +++++++-
 heap_lang/lifting.v | 5 +++--
 2 files changed, 10 insertions(+), 3 deletions(-)

diff --git a/README b/README
index 3a3dd3dcd..53ccfc1bb 100644
--- a/README
+++ b/README
@@ -4,9 +4,15 @@ PREREQUISITES
 This version is known to compile with:
 
  - Coq 8.5
- - Ssreflect >= 3cc0493
+ - Ssreflect 1.6
  - Autosubst 1.4
 
+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
 ---------------------
 
diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index 883d642f6..71116edec 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -21,8 +21,9 @@ Lemma wp_alloc_pst E σ e v Q :
   (ownP σ ★ ▷ (∀ l, ■(σ !! l = None) ∧ ownP (<[l:=v]>σ) -★ Q (LocV l)))
        ⊑ wp E (Alloc e) Q.
 Proof.
-  intros; rewrite -(wp_lift_atomic_step (Alloc e) (λ v' σ' ef,
-    ∃ l, ef = None ∧ v' = LocV l ∧ σ' = <[l:=v]>σ ∧ σ !! l = None) σ) //;
+  (* TODO RJ: This works around ssreflect bug #22. *)
+  intros. set (φ v' σ' ef := ∃ l, ef = @None expr ∧ v' = LocV l ∧ σ' = <[l:=v]>σ ∧ σ !! l = None).
+  rewrite -(wp_lift_atomic_step (Alloc e) φ σ) // /φ;
     last by intros; inv_step; eauto 8.
   apply sep_mono, later_mono; first done.
   apply forall_intro=>e2; apply forall_intro=>σ2; apply forall_intro=>ef.
-- 
GitLab