Bump iris, fix build.

opam

@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"]
 depends: [
-  "coq-iris" { (= "dev.2017-10-28.10") | (= "dev") }
+  "coq-iris" { (= "dev.2018-02-21.1") | (= "dev") }
 ]

theories/barrier/example_client.v

@@ -61,7 +61,7 @@ Section ClosedProofs.
 
 Let Σ : gFunctors := #[ heapΣ ; barrierΣ ; spawnΣ ].
 
-Lemma client_adequate σ : adequate client σ (λ _, True).
+Lemma client_adequate σ : adequate NotStuck client σ (λ _, True).
 Proof. apply (heap_adequacy Σ)=> ?. apply client_safe. Qed.
 
 End ClosedProofs.

theories/barrier/proof.v

@@ -10,9 +10,9 @@ Set Default Proof Using "Type".
 (** The CMRAs/functors we need. *)
 Class barrierG Σ := BarrierG {
   barrier_stsG :> stsG Σ sts;
-  barrier_savedPropG :> savedPropG Σ idCF;
+  barrier_savedPropG :> savedPropG Σ;
 }.
-Definition barrierΣ : gFunctors := #[stsΣ sts; savedPropΣ idCF].
+Definition barrierΣ : gFunctors := #[stsΣ sts; savedPropΣ].
 
 Instance subG_barrierΣ {Σ} : subG barrierΣ Σ → barrierG Σ.
 Proof. solve_inG. Qed.
@@ -62,7 +62,7 @@ Global Instance barrier_inv_ne n l :
   Proper (dist n ==> eq ==> dist n) (barrier_inv l).
 Proof. solve_proper. Qed.
 Global Instance barrier_ctx_ne γ l : NonExpansive (barrier_ctx γ l).
-Proof. solve_proper. Qed. 
+Proof. solve_proper. Qed.
 Global Instance send_ne l : NonExpansive (send l).
 Proof. solve_proper. Qed.
 Global Instance recv_ne l : NonExpansive (recv l).
@@ -94,7 +94,7 @@ Proof.
   iIntros (Φ) "_ HΦ".
   rewrite -wp_fupd /newbarrier /=. wp_seq. wp_alloc l as "Hl".
   iApply ("HΦ" with "[> -]").
-  iMod (saved_prop_alloc (F:=idCF) P) as (γ) "#?".
+  iMod (saved_prop_alloc P) as (γ) "#?".
   iMod (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}) with "[-]")
     as (γ') "[#? Hγ']"; eauto.
   { iNext. rewrite /barrier_inv /=. iFrame.
@@ -165,8 +165,8 @@ Proof.
   iIntros (?). iDestruct 1 as (γ P Q i) "(#Hsts & Hγ & #HQ & HQR)".
   iMod (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]")
     as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto.
-  iMod (saved_prop_alloc_strong (R1: ∙%CF (iProp Σ)) I) as (i1) "[% #Hi1]".
-  iMod (saved_prop_alloc_strong (R2: ∙%CF (iProp Σ)) (I ∪ {[i1]}))
+  iMod (saved_prop_alloc_strong I) as (i1) "[% #Hi1]".
+  iMod (saved_prop_alloc_strong (I ∪ {[i1]}))
     as (i2) "[Hi2' #Hi2]"; iDestruct "Hi2'" as %Hi2.
   rewrite ->not_elem_of_union, elem_of_singleton in Hi2; destruct Hi2.
   iMod ("Hclose" $! (State p ({[i1; i2]} ∪ I ∖ {[i]}))