From dec707daaeb72616e96825b914a1eaa27a5339c5 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 20 May 2018 11:55:08 +0200
Subject: [PATCH] bump Iris, fix build
---
opam | 2 +-
theories/fractor.v | 1 -
theories/persistor.v | 5 +----
3 files changed, 2 insertions(+), 6 deletions(-)
diff --git a/opam b/opam
index 75e892b8..398c658d 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/igps" ]
depends: [
- "coq-iris" { (= "branch.gen_proofmode.2018-04-05.1") | (= "dev") }
+ "coq-iris" { (= "branch.gen_proofmode.2018-05-18.0.ec4ac846") | (= "dev") }
]
diff --git a/theories/fractor.v b/theories/fractor.v
index 5790dd09..ef95e2c5 100644
--- a/theories/fractor.v
+++ b/theories/fractor.v
@@ -70,7 +70,6 @@ Section Fractor.
Proof.
iIntros "[Info1 Info2]".
iCombine "Info1" "Info2" as "Info".
- rewrite op_singleton pair_op.
iDestruct (own_valid with "Info") as %Valid.
apply singleton_valid in Valid.
destruct Valid as [_ Valid2]. simpl in Valid2.
diff --git a/theories/persistor.v b/theories/persistor.v
index 267d23d0..2b9aa771 100644
--- a/theories/persistor.v
+++ b/theories/persistor.v
@@ -91,7 +91,7 @@ Section Persistor.
iDestruct "Per2" as (X2) "[Per2 [#Inv2 #[PerCtx2 PerOwn2]]]".
iCombine "PerOwn1" "PerOwn2" as "PerOwn".
iDestruct (own_valid with "PerOwn") as %Valid.
- move: Valid. rewrite op_singleton => /singleton_valid /agree_op_inv Valid.
+ move: Valid => /singleton_valid /agree_op_inv Valid.
apply (inj to_agree) in Valid. setoid_subst.
iExists X2. iFrame. iFrame "Inv2". by iSplit.
- iIntros "Per".
@@ -110,7 +110,6 @@ Section Persistor.
iDestruct "P2" as (X2) "(P2 & #Inv2 & #PC2 & #oP2)".
iCombine "oP1" "oP2" as "oP".
iDestruct (own_valid with "oP") as %Valid.
- rewrite op_singleton in Valid.
apply singleton_valid, agree_op_inv, (inj to_agree) in Valid. setoid_subst.
iExists X2. iFrame "P1 P2 Inv1 oP1 PC1".
Qed.
@@ -124,7 +123,6 @@ Section Persistor.
iDestruct "P2" as (X2) "(P2 & #Inv2 & #PC2 & #oP2)".
iCombine "oP1" "oP2" as "oP".
iDestruct (own_valid with "oP") as %Valid.
- rewrite op_singleton in Valid.
apply singleton_valid, agree_op_inv, (inj to_agree) in Valid. setoid_subst.
iExists X2. iFrame "P1 P2 Inv2 oP1 PC1".
Qed.
@@ -138,7 +136,6 @@ Section Persistor.
iDestruct "P2" as (X2) "(P2 & #Inv2 & #PC2 & >#oP2)".
iCombine "oP1" "oP2" as "oP".
iDestruct (own_valid with "oP") as %Valid.
- rewrite op_singleton in Valid.
apply singleton_valid, agree_op_inv, (inj to_agree) in Valid. setoid_subst.
iExists X2. iModIntro. iFrame "P1 P2 Inv1 oP1 PC1".
Qed.
--
GitLab