From 2deb5e0dd899a46376db8137a92efdc15cea61f5 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 13 Jun 2019 11:14:34 +0200
Subject: [PATCH] bump Iris
---
opam | 2 +-
theories/logrel/stlc/soundness.v | 1 -
2 files changed, 1 insertion(+), 2 deletions(-)
diff --git a/opam b/opam
index e8fe5ce5..a26355d0 100644
--- a/opam
+++ b/opam
@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"]
depends: [
- "coq-iris" { (= "dev.2019-06-12.4.ae1dd418") | (= "dev") }
+ "coq-iris" { (= "dev.2019-06-13.0.860bd8e4") | (= "dev") }
"coq-autosubst" { = "dev.coq86" }
]
diff --git a/theories/logrel/stlc/soundness.v b/theories/logrel/stlc/soundness.v
index d080562e..3c50d7e1 100644
--- a/theories/logrel/stlc/soundness.v
+++ b/theories/logrel/stlc/soundness.v
@@ -20,4 +20,3 @@ Proof.
set (HΣ := IrisG _ _ Hinv (λ _ _ _, True)%I (λ _, True)%I).
iApply (wp_wand with "[]"). by iApply wp_soundness. eauto.
Qed.
-
--
GitLab