From 355d27d7187ea310759e918585ac1ac5521c84cb Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 25 Jan 2021 20:18:21 +0100
Subject: [PATCH] Bump Iris.
---
coq-lambda-rust.opam | 2 +-
theories/lang/heap.v | 6 +++---
theories/typing/type.v | 4 ++--
3 files changed, 6 insertions(+), 6 deletions(-)
diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index bc8b4867..925241d2 100644
--- a/coq-lambda-rust.opam
+++ b/coq-lambda-rust.opam
@@ -13,7 +13,7 @@ the type system, and safety proof for some Rust libraries.
"""
depends: [
- "coq-iris" { (= "dev.2020-12-10.1.872fe77b") | (= "dev") }
+ "coq-iris" { (= "dev.2021-01-25.1.21b7ffa1") | (= "dev") }
]
build: [make "-j%{jobs}%"]
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index 9ad9af67..5fa2cf3c 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -9,13 +9,13 @@ From lrust.lang Require Export lang.
Set Default Proof Using "Type".
Import uPred.
-Definition lock_stateR : cmraT :=
+Definition lock_stateR : cmra :=
csumR (exclR unitO) natR.
-Definition heapUR : ucmraT :=
+Definition heapUR : ucmra :=
gmapUR loc (prodR (prodR fracR lock_stateR) (agreeR valO)).
-Definition heap_freeableUR : ucmraT :=
+Definition heap_freeableUR : ucmra :=
gmapUR block (prodR fracR (gmapR Z (exclR unitO))).
Class heapG Σ := HeapG {
diff --git a/theories/typing/type.v b/theories/typing/type.v
index b090940d..dcbd4c11 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -190,7 +190,7 @@ Section ofe.
- split; [by destruct 1|by intros [[??] ?]; constructor].
- split; [by destruct 1|by intros [[??] ?]; constructor].
Qed.
- Canonical Structure typeO : ofeT := OfeT type type_ofe_mixin.
+ Canonical Structure typeO : ofe := Ofe type type_ofe_mixin.
Global Instance ty_size_ne n : Proper (dist n ==> eq) ty_size.
Proof. intros ?? EQ. apply EQ. Qed.
@@ -242,7 +242,7 @@ Section ofe.
- split; [by destruct 1|by constructor].
- split; [by destruct 1|by constructor].
Qed.
- Canonical Structure stO : ofeT := OfeT simple_type st_ofe_mixin.
+ Canonical Structure stO : ofe := Ofe simple_type st_ofe_mixin.
Global Instance st_own_ne n :
Proper (dist n ==> eq ==> eq ==> dist n) st_own.
--
GitLab