From 753aaaae2e39896509ea878318858d2e0bc3441f Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Tue, 13 Dec 2016 12:34:35 +0100
Subject: [PATCH] fix build with latest iris

---
 opam.pins              | 2 +-
 theories/atomic_incr.v | 2 +-
 theories/atomic_pcas.v | 4 ++--
 theories/atomic_sync.v | 4 +++-
 theories/evmap.v       | 5 ++++-
 theories/flat.v        | 4 +++-
 theories/misc.v        | 5 +++--
 theories/peritem.v     | 4 +++-
 theories/simple_sync.v | 2 +-
 theories/treiber.v     | 4 +++-
 10 files changed, 24 insertions(+), 12 deletions(-)

diff --git a/opam.pins b/opam.pins
index fd3eb4b..396d747 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 0cc2c6e098bfb05c056783b9212c9218fa46aa5e
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq b212b3faddae4b089f30ef1c7a27d43ebd3a1675
diff --git a/theories/atomic_incr.v b/theories/atomic_incr.v
index 65628b7..e7fa0c9 100644
--- a/theories/atomic_incr.v
+++ b/theories/atomic_incr.v
@@ -66,7 +66,7 @@ Section user.
   Lemma incr_2_safe:
     ∀ (x: Z), (WP incr_2 #x {{ _, True }})%I.
   Proof.
-    iIntros (x) "". (* FIXME: I did iIntros, this should not be needed. *)
+    iIntros (x).
     rewrite /incr_2 /=.
     wp_lam.
     wp_alloc l as "Hl".
diff --git a/theories/atomic_pcas.v b/theories/atomic_pcas.v
index 63358e3..103a57d 100644
--- a/theories/atomic_pcas.v
+++ b/theories/atomic_pcas.v
@@ -1,13 +1,13 @@
 From iris.program_logic Require Export weakestpre hoare.
 From iris.heap_lang Require Export lang proofmode notation.
 From iris.heap_lang.lib Require Import spin_lock.
-From iris.algebra Require Import dec_agree frac.
+From iris.algebra Require Import agree frac.
 From iris_atomic Require Import sync atomic_sync.
 Import uPred.
 
 Section atomic_pair.
   Context `{!heapG Σ, !lockG Σ, !syncG Σ,
-            !inG Σ (prodR fracR (dec_agreeR (val * val)))} (N : namespace).
+            !inG Σ (prodR fracR (agreeR (prodC valC valC)))} (N : namespace).
   
   Definition pcas_seq : val :=
     λ: "ls" "ab",
diff --git a/theories/atomic_sync.v b/theories/atomic_sync.v
index 7c2906c..b716dde 100644
--- a/theories/atomic_sync.v
+++ b/theories/atomic_sync.v
@@ -2,9 +2,11 @@
 From iris.program_logic Require Export weakestpre hoare.
 From iris.heap_lang Require Export lang proofmode notation.
 From iris.heap_lang.lib Require Import spin_lock.
-From iris.algebra Require Import dec_agree frac.
+From iris.algebra Require Import deprecated frac.
 From iris_atomic Require Import atomic sync misc.
 
+Import dec_agree.
+
 Definition syncR := prodR fracR (dec_agreeR val). (* track the local knowledge of ghost state *)
 Class syncG Σ := sync_tokG :> inG Σ syncR.
 Definition syncΣ : gFunctors := #[GFunctor (constRF syncR)].
diff --git a/theories/evmap.v b/theories/evmap.v
index 6dabdd8..48a65f1 100644
--- a/theories/evmap.v
+++ b/theories/evmap.v
@@ -1,9 +1,12 @@
 (* evmap.v -- generalized heap-like monoid composite *)
 From iris.base_logic Require Export invariants.
 From iris.program_logic Require Export weakestpre.
-From iris.algebra Require Export auth frac gmap dec_agree.
+From iris.algebra Require Export auth frac gmap.
+From iris.algebra Require deprecated.
 From iris.proofmode Require Import tactics.
 
+Export deprecated.dec_agree.
+
 Section evmap.
   Context (K A: Type) (Q: cmraT) `{Countable K, EqDecision A}.
   Definition evkR := prodR Q (dec_agreeR A).
diff --git a/theories/flat.v b/theories/flat.v
index 39b4370..c5aa9c3 100644
--- a/theories/flat.v
+++ b/theories/flat.v
@@ -4,10 +4,12 @@ From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
 From iris.heap_lang.lib Require Import spin_lock.
-From iris.algebra Require Import auth frac agree excl dec_agree gset gmap.
+From iris.algebra Require Import auth frac agree excl deprecated gset gmap.
 From iris.base_logic Require Import big_op saved_prop.
 From iris_atomic Require Import misc peritem sync evmap.
 
+Import dec_agree.
+
 Definition doOp : val :=
   λ: "p",
      match: !"p" with
diff --git a/theories/misc.v b/theories/misc.v
index 7d1b326..bc4be1c 100644
--- a/theories/misc.v
+++ b/theories/misc.v
@@ -2,10 +2,11 @@
 
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang proofmode notation.
-From iris.algebra Require Import auth frac gmap dec_agree.
+From iris.algebra Require Import auth frac gmap deprecated.
 From iris.prelude Require Import countable.
 From iris.base_logic Require Import big_op auth fractional.
-Import uPred.
+
+Import uPred dec_agree.
 
 Section lemmas.
   Lemma pair_l_frac_op' (p q: Qp) (g g': val):
diff --git a/theories/peritem.v b/theories/peritem.v
index a506380..c0143bb 100644
--- a/theories/peritem.v
+++ b/theories/peritem.v
@@ -1,10 +1,12 @@
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
-From iris.algebra Require Import frac auth gmap dec_agree csum.
+From iris.algebra Require Import frac auth gmap deprecated csum.
 From iris.base_logic Require Import big_op.
 From iris_atomic Require Export treiber misc evmap.
 
+Import dec_agree.
+
 Section defs.
   Context `{heapG Σ, !evidenceG loc val unitR Σ} (N: namespace).
   Context (R: val → iProp Σ) `{∀ x, TimelessP (R x)}.
diff --git a/theories/simple_sync.v b/theories/simple_sync.v
index 50b11a9..c15ce1e 100644
--- a/theories/simple_sync.v
+++ b/theories/simple_sync.v
@@ -3,7 +3,7 @@
 From iris.program_logic Require Export weakestpre hoare.
 From iris.heap_lang Require Export lang proofmode notation.
 From iris.heap_lang.lib Require Import spin_lock.
-From iris.algebra Require Import dec_agree frac.
+From iris.algebra Require Import frac.
 From iris_atomic Require Import sync.
 Import uPred.
 
diff --git a/theories/treiber.v b/theories/treiber.v
index 817c085..c1db56b 100644
--- a/theories/treiber.v
+++ b/theories/treiber.v
@@ -1,10 +1,12 @@
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
-From iris.algebra Require Import frac auth gmap dec_agree csum.
+From iris.algebra Require Import frac auth gmap deprecated csum.
 From iris.base_logic Require Import big_op.
 From iris_atomic Require Import atomic misc.
 
+Import dec_agree.
+
 Definition new_stack: val := λ: <>, ref (ref NONE).
 
 Definition push: val :=
-- 
GitLab