From 03fc47627cfcc20bfddf9d62d6c2de1648976d67 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 27 May 2020 08:29:46 +0200
Subject: [PATCH] update dependencies, fix for lifting rename
---
opam | 2 +-
theories/examples/coinflip.v | 2 +-
theories/examples/lateearlychoice.v | 2 +-
theories/examples/ticket_lock.v | 6 +++---
theories/logic/model.v | 3 +--
theories/logic/spec_ra.v | 2 +-
6 files changed, 8 insertions(+), 9 deletions(-)
diff --git a/opam b/opam
index 3023744..4ca4f67 100644
--- a/opam
+++ b/opam
@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/reloc"]
depends: [
- "coq-iris" { (= "dev.2020-05-26.0.e3f87a95") | (= "dev") }
+ "coq-iris" { (= "dev.2020-05-26.1.d80e7abf") | (= "dev") }
"coq-autosubst" { = "dev.coq86" }
]
diff --git a/theories/examples/coinflip.v b/theories/examples/coinflip.v
index 2631e0a..eed47d8 100644
--- a/theories/examples/coinflip.v
+++ b/theories/examples/coinflip.v
@@ -1,4 +1,4 @@
-From iris.heap_lang Require Import lifting.
+From iris.heap_lang Require Import derived_laws.
From reloc Require Import reloc lib.lock.
(* for rand (), val_to_bool *)
diff --git a/theories/examples/lateearlychoice.v b/theories/examples/lateearlychoice.v
index 80f6394..b4eb8d4 100644
--- a/theories/examples/lateearlychoice.v
+++ b/theories/examples/lateearlychoice.v
@@ -1,4 +1,4 @@
-From iris.heap_lang Require Import lifting.
+From iris.heap_lang Require Import derived_laws.
From reloc Require Import reloc.
Definition rand: val :=
diff --git a/theories/examples/ticket_lock.v b/theories/examples/ticket_lock.v
index c5a8257..edecad1 100644
--- a/theories/examples/ticket_lock.v
+++ b/theories/examples/ticket_lock.v
@@ -187,7 +187,7 @@ Section refinement.
iMod (issueNewTicket with "Hissued") as "[Hissued Hm]".
iMod ("H" with "[-HP Hm]") as "_".
{ iExists _. iFrame.
- replace (Z.of_nat n + 1) with (Z.of_nat (S n)) by lia.
+ replace (Z.of_nat n + 1)%Z with (Z.of_nat (S n)) by lia.
done. }
clear o o'.
repeat rel_pure_l.
@@ -259,7 +259,7 @@ Section refinement.
iMod (issueNewTicket with "Hissued") as "[Hissued Hm]".
iMod ("Hcl" with "[-Hm]") as "_".
{ iNext.
- replace (Z.of_nat n + 1) with (Z.of_nat (S n)) by lia.
+ replace (Z.of_nat n + 1)%Z with (Z.of_nat (S n)) by lia.
iExists _,_,_; by iFrame. }
repeat rel_pure_l.
by iApply wait_loop_refinement.
@@ -335,7 +335,7 @@ Section refinement.
iIntros "Hl'".
iMod ("Hcl" with "[-]") as "_".
{ iNext.
- replace (o' + 1) with (Z.of_nat (o' + 1))%nat by lia.
+ replace (o' + 1)%Z with (Z.of_nat (o' + 1))%nat by lia.
iExists (o' + 1)%nat,_,_. by iFrame. }
rel_values.
Qed.
diff --git a/theories/logic/model.v b/theories/logic/model.v
index cfc792d..a5b808d 100644
--- a/theories/logic/model.v
+++ b/theories/logic/model.v
@@ -3,10 +3,9 @@
- The model for types and type combinators;
- Closure under context substitutions;
- Basic monadic rules *)
-From iris.heap_lang Require Export lifting metatheory.
From iris.base_logic.lib Require Import invariants.
From iris.algebra Require Import list gmap.
-From iris.heap_lang Require Export lang notation.
+From iris.heap_lang Require Export lang notation derived_laws metatheory.
From iris.heap_lang Require Import proofmode.
From reloc Require Import prelude.properness logic.spec_rules prelude.ctx_subst.
From reloc Require Export logic.spec_ra.
diff --git a/theories/logic/spec_ra.v b/theories/logic/spec_ra.v
index d9e1754..90dcc44 100644
--- a/theories/logic/spec_ra.v
+++ b/theories/logic/spec_ra.v
@@ -5,7 +5,7 @@ From iris.bi Require Export fractional.
From iris.base_logic Require Import gen_heap.
From iris.base_logic Require Export invariants.
From iris.proofmode Require Import tactics.
-From iris.heap_lang Require Import lang lifting.
+From iris.heap_lang Require Import lang primitive_laws.
Import uPred.
Definition relocN := nroot .@ "reloc".
--
GitLab