From e35e4af67a7673eec0e6533603de4240a9204de1 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 2 May 2019 08:27:58 +0200
Subject: [PATCH] Bump Iris.
---
opam | 2 +-
theories/lang/heap.v | 2 +-
theories/lifetime/model/primitive.v | 2 +-
theories/typing/lft_contexts.v | 2 +-
4 files changed, 4 insertions(+), 4 deletions(-)
diff --git a/opam b/opam
index 6e9e09bb..a33985ab 100644
--- a/opam
+++ b/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.2019-04-25.1.a9031f7f") | (= "dev") }
+ "coq-iris" { (= "dev.2019-05-01.1.c7164230") | (= "dev") }
]
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index 38b14062..2c3acda7 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -129,7 +129,7 @@ Section heap.
Global Instance heap_mapsto_vec_fractional l vl: Fractional (λ q, l ↦∗{q} vl)%I.
Proof.
- intros p q. rewrite /heap_mapsto_vec -big_sepL_sepL.
+ intros p q. rewrite /heap_mapsto_vec -big_sepL_sep.
by setoid_rewrite (fractional (Φ := λ q, _ ↦{q} _)%I).
Qed.
Global Instance heap_mapsto_vec_as_fractional l q vl:
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index c633f1dd..4086a824 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -289,7 +289,7 @@ Proof. rewrite /lft_dead. iDestruct 1 as (Λ) "[% H']". set_solver. Qed.
(* Fractional and AsFractional instances *)
Global Instance lft_tok_fractional κ : Fractional (λ q, q.[κ])%I.
Proof.
- intros p q. rewrite /lft_tok -big_sepMS_sepMS. apply big_sepMS_proper.
+ intros p q. rewrite /lft_tok -big_sepMS_sep. apply big_sepMS_proper.
intros Λ ?. rewrite -Cinl_op -op_singleton auth_frag_op own_op //.
Qed.
Global Instance lft_tok_as_fractional κ q :
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index eead3bd4..89829f2e 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -60,7 +60,7 @@ Section lft_contexts.
Global Arguments llctx_interp _ _%Qp.
Global Instance llctx_interp_fractional L :
Fractional (llctx_interp L).
- Proof. intros ??. rewrite -big_sepL_sepL. by setoid_rewrite <-fractional. Qed.
+ Proof. intros ??. rewrite -big_sepL_sep. by setoid_rewrite <-fractional. Qed.
Global Instance llctx_interp_as_fractional L q :
AsFractional (llctx_interp L q) (llctx_interp L) q.
Proof. split. done. apply _. Qed.
--
GitLab