From b56c7cc7673bf376d61de653f26c67367dcb9d8a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 24 May 2020 11:28:06 +0200
Subject: [PATCH] Bump Iris (sbi removal).
---
opam | 2 +-
theories/logic/model.v | 6 ++----
2 files changed, 3 insertions(+), 5 deletions(-)
diff --git a/opam b/opam
index febee4c..bb2473f 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-18.2.fdda97e8") | (= "dev") }
+ "coq-iris" { (= "dev.2020-05-24.1.76bec8b7") | (= "dev") }
"coq-autosubst" { = "dev.coq86" }
]
diff --git a/theories/logic/model.v b/theories/logic/model.v
index 44417a6..ae804f7 100644
--- a/theories/logic/model.v
+++ b/theories/logic/model.v
@@ -102,10 +102,8 @@ Section semtypes.
Instance lrel_rec1_contractive C : Contractive (lrel_rec1 C).
Proof.
intros n. intros P Q HPQ.
- unfold lrel_rec1. intros w1 w2.
- apply bi.later_contractive.
- destruct n; try done.
- simpl in HPQ; simpl. f_equiv. by apply C.
+ unfold lrel_rec1. intros w1 w2. rewrite {1 4}/lrel_car /=.
+ f_contractive. f_equiv. by apply C.
Qed.
Definition lrel_rec (C : lrelC Σ -n> lrelC Σ) : lrel Σ := fixpoint (lrel_rec1 C).
--
GitLab