From f32cecf4d1429dc882ad3b842ec50d0e8bde181b Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Wed, 5 May 2021 21:54:35 +0200
Subject: [PATCH] Update dependencies

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

diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index 6004d44f..87077311 100644
--- a/coq-lambda-rust.opam
+++ b/coq-lambda-rust.opam
@@ -15,7 +15,7 @@ This branch uses a proper weak memory model.
 """
 
 depends: [
-  "coq-gpfsl" { (= "dev.2021-04-20.0.13632051") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2021-05-05.0.6c5a80f0") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 782dd346..b0fe6d6d 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -409,7 +409,7 @@ Section typing.
   Proof.
     iIntros (<- ->) "#Hbody /=". iIntros (tid) "#LFT _ $ $ #HT". iApply wp_value.
     rewrite tctx_interp_singleton. iLöb as "IH". iExists _. iSplit.
-    { unlock. rewrite /= decide_left. done. }
+    { unlock. rewrite /= decide_True_pi. done. }
     iExists fb, _, argsb, e, _. iSplit. done. iSplit. done. iNext.
     iIntros (x ϝ k args) "!#". iIntros (tid') "_ 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 95327226..faa9344a 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -34,7 +34,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 tid p v (SUB : ↑histN ⊆ E) :
     eval_path p = Some v → ⊢ WP p in tid @ E {{ v', ⌜v' = v⌝ }}.
-- 
GitLab