From 4a54b63f2a60fffba0e7ad9f404a1cece8a49d6e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 11 Mar 2020 10:25:10 +0100
Subject: [PATCH] Bump Iris.
---
opam | 2 +-
theories/lang/races.v | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/opam b/opam
index eb3bb013..705e3802 100644
--- a/opam
+++ b/opam
@@ -14,7 +14,7 @@ the type system, and safety proof for some Rust libraries.
"""
depends: [
- "coq-iris" { (= "dev.2020-02-25.3.bb9152ec") | (= "dev") }
+ "coq-iris" { (= "dev.2020-03-10.6.79f576aa") | (= "dev") }
]
build: [make "-j%{jobs}%"]
diff --git a/theories/lang/races.v b/theories/lang/races.v
index 79da2aa6..35044a02 100644
--- a/theories/lang/races.v
+++ b/theories/lang/races.v
@@ -75,7 +75,7 @@ Lemma next_access_head_reductible_ctx e σ σ' a l K :
next_access_head e σ' a l → reducible (fill K e) σ → head_reducible e σ.
Proof.
intros Hhead Hred. apply prim_head_reducible.
- - eapply (reducible_fill (K:=ectx_language.fill K)), Hred. destruct Hhead; eauto.
+ - eapply (reducible_fill_inv (K:=ectx_language.fill K)), Hred. destruct Hhead; eauto.
- apply ectxi_language_sub_redexes_are_values. intros [] ? ->; inversion Hhead; eauto.
Qed.
--
GitLab