From 19719b78f91111e87eaafe1c42c4ef703f0e0b7a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 13 May 2020 10:30:05 +0200
Subject: [PATCH] Bump Iris.
---
opam | 2 +-
theories/utils/llist.v | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/opam b/opam
index 2666779..43358e0 100644
--- a/opam
+++ b/opam
@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/actris" ]
depends: [
- "coq-iris" { (= "dev.2020-04-24.0.9cc3cc77") | (= "dev") }
+ "coq-iris" { (= "dev.2020-05-13.0.635cdf1e") | (= "dev") }
]
diff --git a/theories/utils/llist.v b/theories/utils/llist.v
index dcce8a7..aedd266 100644
--- a/theories/utils/llist.v
+++ b/theories/utils/llist.v
@@ -242,7 +242,7 @@ Lemma lsplit_spec l xs :
Proof.
iIntros (Φ) "Hl HΦ". wp_lam.
wp_apply (llength_spec with "Hl"); iIntros "Hl". wp_pures.
- rewrite Z.quot_div_nonneg; [|lia..]. rewrite -(Z2Nat_inj_div _ 2).
+ rewrite Z.quot_div_nonneg; [|lia..]. rewrite -(Nat2Z_inj_div _ 2).
wp_apply (lsplit_at_spec with "Hl"); iIntros (k) "[Hl Hk]".
iApply "HΦ". iFrame. by rewrite take_drop.
Qed.
--
GitLab