diff --git a/opam b/opam
index eb3bb013053bfc70f486f93651f27b76c24ff857..705e38026aaa3f64abc1f3d9aa514e9540fd3501 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 79da2aa65fe3be9e82592f5160c16f255da165b9..35044a021429ee59321637384e4bc62e2ed28a16 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.