From 811a208104a768a444266dd4edd1c353e2429854 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 16 Jun 2018 09:58:00 +0200
Subject: [PATCH] bump Iris; fix build
---
opam | 2 +-
theories/adequacy.v | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/opam b/opam
index 9327471f..639056c0 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-06-14.8.bf9fd4f5") | (= "dev") }
+ "coq-iris" { (= "branch.gen_proofmode.2018-06-15.3.d88d654b") | (= "dev") }
]
diff --git a/theories/adequacy.v b/theories/adequacy.v
index a5ef9c8f..5308ce4c 100644
--- a/theories/adequacy.v
+++ b/theories/adequacy.v
@@ -222,7 +222,7 @@ Proof.
iCombine "A" "B" as "AB".
rewrite (big_sepM_fmap _ _ (to_hist σ)). rewrite -big_sepM_sepM.
match goal with
- | |- coq_tactics.envs_entails _ (big_opM _ ?f ?g) =>
+ | |- environments.envs_entails _ (big_opM _ ?f ?g) =>
iApply (big_sepM_impl _ f with "[$AB]")
end.
iIntros "!#". iIntros (? ? ?) "[A B]". destruct a0.
--
GitLab