bump Iris

opam

@@ -11,5 +11,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
 depends: [
-  "coq-iris" { (= "dev.2018-10-04.1.5e608261") | (= "dev") }
+  "coq-iris" { (= "dev.2018-10-04.7.fc21b664") | (= "dev") }
 ]

theories/lang/adequacy.v

@@ -19,7 +19,7 @@ Proof. solve_inG. Qed.
 
 Definition lrust_adequacy Σ `{lrustPreG Σ} e σ φ :
   (∀ `{lrustG Σ}, True ⊢ WP e {{ v, ⌜φ v⌝ }}) →
-  adequate NotStuck e σ φ.
+  adequate NotStuck e σ (λ v _, φ v).
 Proof.
   intros Hwp; eapply (wp_adequacy _ _); iIntros (?) "".
   iMod (own_alloc (● to_heap σ)) as (vγ) "Hvγ".

theories/typing/soundness.v

@@ -31,7 +31,7 @@ Section type_soundness.
     (∀ e, e ∈ t → is_Some (to_val e) ∨ reducible e σ).
   Proof.
     intros Hmain Hrtc.
-    cut (adequate NotStuck (main [exit_cont]%E) ∅ (λ _, True)).
+    cut (adequate NotStuck (main [exit_cont]%E) ∅ (λ _ _, True)).
     { split. by eapply adequate_nonracing.
       intros. by eapply (adequate_not_stuck _ (main [exit_cont]%E)). }
     apply: lrust_adequacy=>?. iIntros "_".