Merge branch 'master' of gitlab.mpi-sws.org:iris/lambda-rust

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}%"]

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.