From 10b7a540996c81e7f9aa92431517f920a96bc515 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 6 Feb 2017 17:04:22 +0100
Subject: [PATCH] update iris to use stdpp
---
opam.pins | 2 +-
theories/lang/heap.v | 2 +-
theories/lang/lang.v | 4 ++--
theories/lang/races.v | 2 +-
theories/lang/tactics.v | 2 +-
theories/lifetime/lifetime_sig.v | 2 +-
theories/typing/unsafe/refcell/ref_code.v | 4 ++--
theories/typing/unsafe/refcell/refcell_code.v | 2 +-
theories/typing/unsafe/refcell/refmut_code.v | 2 +-
9 files changed, 11 insertions(+), 11 deletions(-)
diff --git a/opam.pins b/opam.pins
index 642f2e56..8868ac83 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq b0418bd57b9341dbf5e58669c689201daa561bd7
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq b863cfd7640f5dccb14c17e9ffefb475f1b7d0d8
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index b5c53cd3..f3f69a16 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -1,5 +1,5 @@
From Coq Require Import Min.
-From iris.prelude Require Import coPset.
+From stdpp Require Import coPset.
From iris.algebra Require Import cmra_big_op gmap frac agree.
From iris.algebra Require Import csum excl auth.
From iris.base_logic Require Import big_op lib.fractional.
diff --git a/theories/lang/lang.v b/theories/lang/lang.v
index e770632f..96df4989 100644
--- a/theories/lang/lang.v
+++ b/theories/lang/lang.v
@@ -1,6 +1,6 @@
From iris.program_logic Require Export language ectx_language ectxi_language.
-From iris.prelude Require Export strings.
-From iris.prelude Require Import gmap.
+From stdpp Require Export strings.
+From stdpp Require Import gmap.
Set Default Proof Using "Type".
Open Scope Z_scope.
diff --git a/theories/lang/races.v b/theories/lang/races.v
index 1ba1a13f..6cc6f95b 100644
--- a/theories/lang/races.v
+++ b/theories/lang/races.v
@@ -1,4 +1,4 @@
-From iris.prelude Require Import gmap.
+From stdpp Require Import gmap.
From iris.program_logic Require Export hoare.
From iris.program_logic Require Import adequacy.
From lrust.lang Require Import tactics.
diff --git a/theories/lang/tactics.v b/theories/lang/tactics.v
index 99dc7464..7ebfc8c5 100644
--- a/theories/lang/tactics.v
+++ b/theories/lang/tactics.v
@@ -1,4 +1,4 @@
-From iris.prelude Require Import fin_maps.
+From stdpp Require Import fin_maps.
From lrust.lang Require Export lang.
Set Default Proof Using "Type".
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index c6171e0b..4684b65d 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -1,5 +1,5 @@
From iris.algebra Require Import frac.
-From iris.prelude Require Export gmultiset strings.
+From stdpp Require Export gmultiset strings.
From iris.base_logic.lib Require Export invariants.
From iris.base_logic.lib Require Import boxes fractional.
Set Default Proof Using "Type".
diff --git a/theories/typing/unsafe/refcell/ref_code.v b/theories/typing/unsafe/refcell/ref_code.v
index c373300d..ac08fb9d 100644
--- a/theories/typing/unsafe/refcell/ref_code.v
+++ b/theories/typing/unsafe/refcell/ref_code.v
@@ -182,7 +182,7 @@ Section ref_functions.
- destruct Heq as [?%leibniz_equiv ?%leibniz_equiv]. simpl in *. subst.
iExists None. iFrame. iMod (own_update with "Hâ—â—¯") as "$".
{ apply auth_update_dealloc. rewrite -(right_id None op (Some _)).
- apply op_local_update_cancellable_empty, _. }
+ apply cancel_local_update_empty, _. }
iApply "H†". replace 1%Qp with (q'+q'')%Qp by naive_solver. iFrame.
- destruct Hincl as [ [=] |[ (?&?&[=]&?) | (?&?&[=<-]&[=<-]&[[q0 n']EQ]) ]].
destruct EQ as [?%leibniz_equiv ?%leibniz_equiv]. simpl in *. subst.
@@ -191,7 +191,7 @@ Section ref_functions.
iExists (Some (_, Cinr (q0, n'))). iFrame. iMod (own_update with "Hâ—â—¯") as "$".
{ apply auth_update_dealloc.
rewrite -(agree_idemp (to_agree _)) -pair_op -Cinr_op -pair_op Some_op.
- apply (op_local_update_cancellable_empty (reading_st q ν)), _. }
+ apply (cancel_local_update_empty (reading_st q ν)), _. }
iExists ν. iFrame. iApply step_fupd_intro; first done. iIntros "!>".
iSplitR; first done. iExists (q+q'')%Qp. iFrame.
by rewrite assoc (comm _ q0 q). }
diff --git a/theories/typing/unsafe/refcell/refcell_code.v b/theories/typing/unsafe/refcell/refcell_code.v
index 396076aa..fa185e27 100644
--- a/theories/typing/unsafe/refcell/refcell_code.v
+++ b/theories/typing/unsafe/refcell/refcell_code.v
@@ -184,7 +184,7 @@ Section refcell_functions.
{ apply auth_update_alloc,
(op_local_update_discrete _ _ (reading_st (q'/2)%Qp ν))=>-[Hagv _].
split; [|split].
- - by rewrite -Hag /= agree_idemp.
+ - by rewrite /= -Hag agree_idemp.
- change ((q'/2+q)%Qp ≤ 1%Qp)%Qc. rewrite -Hqq' comm -{2}(Qp_div_2 q').
apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (q'/2)%Qp).
apply Qcplus_le_mono_r, Qp_ge_0.
diff --git a/theories/typing/unsafe/refcell/refmut_code.v b/theories/typing/unsafe/refcell/refmut_code.v
index 8d29b53c..32ff0c6c 100644
--- a/theories/typing/unsafe/refcell/refmut_code.v
+++ b/theories/typing/unsafe/refcell/refmut_code.v
@@ -147,7 +147,7 @@ Section refmut_functions.
iMod ("Hcloseβ" with ">[H↦lrc H◠H◯ Hb] Hna") as "[Hβ Hna]".
{ iExists None. iFrame. iMod (own_update_2 with "Hâ— Hâ—¯") as "$"; last done.
apply auth_update_dealloc. rewrite -(right_id None _ (Some _)).
- apply op_local_update_cancellable_empty, _. }
+ apply cancel_local_update_empty, _. }
iMod ("Hcloseα" with "Hβ") as "Hα". wp_seq.
iAssert (elctx_interp [☀ α] qE) with "[Hα]" as "HE".
{ by rewrite /elctx_interp big_sepL_singleton. }
--
GitLab