From 1cb930d8d10cc9c0555c11b739b9888f3b0d7245 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Sun, 1 May 2016 20:09:39 -0400
Subject: [PATCH] Fixes for Coq 8.4

---
 ConcurrentSeparationLogic.v          | 30 +++++++++++++++-------------
 ConcurrentSeparationLogic_template.v | 21 ++++++++++---------
 2 files changed, 28 insertions(+), 23 deletions(-)

diff --git a/ConcurrentSeparationLogic.v b/ConcurrentSeparationLogic.v
index 6ffb0dd..9da4118 100644
--- a/ConcurrentSeparationLogic.v
+++ b/ConcurrentSeparationLogic.v
@@ -662,12 +662,12 @@ Proof.
   fork (emp%sep) (emp%sep); ht.
 
   loop_inv (fun o => [| isEven (valueOf o) = true |]%sep).
-  erewrite (linkedList_nonnull _ f).
+  match goal with
+  | [ H : r = 0 -> False |- _ ] => erewrite (linkedList_nonnull _ H)
+  end.
   cancel.
   simp.
-  rewrite e, e0.
-  simp.
-  simp.
+  apply andb_true_iff; propositional.
   cancel.
   cancel.
   cancel.
@@ -768,12 +768,12 @@ Proof.
   fork (emp%sep) (emp%sep); ht.
 
   loop_inv (fun o => [| isEven (valueOf o) = true |]%sep).
-  erewrite (linkedList_nonnull _ f).
+  match goal with
+  | [ H : r = 0 -> False |- _ ] => erewrite (linkedList_nonnull _ H)
+  end.
   cancel.
   simp.
-  rewrite e, e0.
-  simp.
-  simp.
+  apply andb_true_iff; propositional.
   cancel.
   cancel.
   cancel.
@@ -1314,7 +1314,7 @@ Proof.
 Qed.
 
 Lemma guarded_impl : forall P Q p,
-    P <-> Q
+    (P <-> Q)
     -> (P ===> p) ===> (Q ===> p).
 Proof.
   simp.
@@ -1333,7 +1333,7 @@ Lemma lockChunks_lock' : forall l I linvs (f : nat -> nat) a,
 Proof.
   induct linvs; simplify.
 
-  cases a; simplify; equality.
+  cases a; simplify; try unfold error in *; equality.
 
   cases a0; simplify.
   invert H0.
@@ -1376,7 +1376,7 @@ Lemma lockChunks_unlock' : forall l I linvs (f : nat -> nat) a,
 Proof.
   induct linvs; simplify.
 
-  cases a; simplify; equality.
+  cases a; simplify; try unfold error in *; equality.
 
   cases a0; simplify.
   invert H0.
@@ -1645,8 +1645,10 @@ Proof.
   simp.
   cases (notAboutToFail c0); auto.
   eapply hoare_triple_notAboutToFail in Heq; eauto.
-  apply use_himp with (Q := [| False |]%sep) in H3.
-  invert H3; propositional.
+  assert ([| False |]%sep f).
+  apply use_himp with (x * lockChunks s linvs)%sep.
   rewrite Heq.
-  cancel.
+  apply False_star.
+  assumption.
+  invert H2; propositional.
 Qed.
diff --git a/ConcurrentSeparationLogic_template.v b/ConcurrentSeparationLogic_template.v
index 0b5f207..410bb30 100644
--- a/ConcurrentSeparationLogic_template.v
+++ b/ConcurrentSeparationLogic_template.v
@@ -684,11 +684,12 @@ Proof.
   fork (emp%sep) (emp%sep); ht.
 
   loop_inv (fun o => [| isEven (valueOf o) = true |]%sep).
-  erewrite (linkedList_nonnull _ f).
+  match goal with
+  | [ H : r = 0 -> False |- _ ] => erewrite (linkedList_nonnull _ H)
+  end.
   cancel.
   simp.
-  rewrite e, e0.
-  simp.
+  apply andb_true_iff; propositional.
   cancel.
   cancel.
   cancel.
@@ -1216,7 +1217,7 @@ Proof.
 Qed.
 
 Lemma guarded_impl : forall P Q p,
-    P <-> Q
+    (P <-> Q)
     -> (P ===> p) ===> (Q ===> p).
 Proof.
   simp.
@@ -1235,7 +1236,7 @@ Lemma lockChunks_lock' : forall l I linvs (f : nat -> nat) a,
 Proof.
   induct linvs; simplify.
 
-  cases a; simplify; equality.
+  cases a; simplify; try unfold error in *; equality.
 
   cases a0; simplify.
   invert H0.
@@ -1278,7 +1279,7 @@ Lemma lockChunks_unlock' : forall l I linvs (f : nat -> nat) a,
 Proof.
   induct linvs; simplify.
 
-  cases a; simplify; equality.
+  cases a; simplify; try unfold error in *; equality.
 
   cases a0; simplify.
   invert H0.
@@ -1547,8 +1548,10 @@ Proof.
   simp.
   cases (notAboutToFail c0); auto.
   eapply hoare_triple_notAboutToFail in Heq; eauto.
-  apply use_himp with (Q := [| False |]%sep) in H3.
-  invert H3; propositional.
+  assert ([| False |]%sep f).
+  apply use_himp with (x * lockChunks s linvs)%sep.
   rewrite Heq.
-  cancel.
+  apply False_star.
+  assumption.
+  invert H2; propositional.
 Qed.