From ec6af5ad3015f515b65a8769adbfe46bc0a431af Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 5 May 2021 09:54:42 +0200
Subject: [PATCH] update dependencies

---
 coq-lambda-rust.opam           | 2 +-
 theories/lang/tactics.v        | 2 +-
 theories/typing/function.v     | 2 +-
 theories/typing/type_context.v | 2 +-
 4 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index 35fef32b..a742e338 100644
--- a/coq-lambda-rust.opam
+++ b/coq-lambda-rust.opam
@@ -13,7 +13,7 @@ the type system, and safety proof for some Rust libraries.
 """
 
 depends: [
-  "coq-iris" { (= "dev.2021-04-20.0.7a260d80") | (= "dev") }
+  "coq-iris" { (= "dev.2021-05-02.0.6a1f68dc") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lang/tactics.v b/theories/lang/tactics.v
index e49c8111..f20d3db1 100644
--- a/theories/lang/tactics.v
+++ b/theories/lang/tactics.v
@@ -207,7 +207,7 @@ Proof.
   apply strongly_atomic_atomic, ectx_language_atomic.
   - inversion 1. naive_solver.
   - apply ectxi_language_sub_redexes_are_values. intros [] * Hskip; try naive_solver.
-    + inversion Hskip. simpl. rewrite decide_left. eauto.
+    + inversion Hskip. simpl. rewrite decide_True_pi. eauto.
     + inversion Hskip. rename select ([Lit _] = _) into Hargs.
       assert (length [Lit LitPoison] = 1%nat) as Hlen by done. move:Hlen.
       rewrite Hargs. rewrite app_length fmap_length /=.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 53f469b3..688d22ca 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -417,7 +417,7 @@ Section typing.
   Proof.
     iIntros (<- ->) "#Hbody /=". iIntros (tid qmax) "#LFT _ $ $ #HT". iApply wp_value.
     rewrite tctx_interp_singleton. iLöb as "IH". iExists _. iSplit.
-    { simpl. rewrite decide_left. done. }
+    { simpl. rewrite decide_True_pi. done. }
     iExists fb, _, argsb, e, _. iSplit; first done. iSplit; first done. iNext.
     iIntros (x ϝ k args) "!>". iIntros (tid' qmax') "_ HE Htl HL HC HT'".
     iApply ("Hbody" with "LFT HE Htl HL HC").
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index d77939a3..b0fb3cb2 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -33,7 +33,7 @@ Section type_context.
 
   Lemma eval_path_of_val (v : val) :
     eval_path v = Some v.
-  Proof. destruct v. done. simpl. rewrite (decide_left _). done. Qed.
+  Proof. destruct v. done. simpl. rewrite (decide_True_pi _). done. Qed.
 
   Lemma wp_eval_path E p v :
     eval_path p = Some v → ⊢ WP p @ E {{ v', ⌜v' = v⌝ }}.
-- 
GitLab