From 174d9053efb7aa683e71415a589822c0f24b9439 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 14 Oct 2023 10:46:28 +0200
Subject: [PATCH] Bump.

---
 coq-lambda-rust.opam             | 2 +-
 theories/lifetime/model/faking.v | 3 +--
 2 files changed, 2 insertions(+), 3 deletions(-)

diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index 1a16b6ab..aed9d929 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.2023-10-03.0.41e501bd") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2023-10-14.0.18d22854") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lifetime/model/faking.v b/theories/lifetime/model/faking.v
index 4c7d0168..62b7420b 100644
--- a/theories/lifetime/model/faking.v
+++ b/theories/lifetime/model/faking.v
@@ -57,8 +57,7 @@ Proof.
     { intros Λ. rewrite lookup_op lookup_gset_to_gmap !lookup_fmap lookup_union_with
         lookup_gset_to_gmap.
       destruct (A !! Λ) eqn:EQ.
-      - apply elem_of_dom_2 in EQ.
-        rewrite [X in _ ≡ X ⋅ _]option_guard_False; last set_solver. by destruct mguard.
+      - apply elem_of_dom_2 in EQ. repeat case_guard; set_solver.
       - apply not_elem_of_dom in EQ.
         destruct (decide (Λ ∈ dom κ)).
         + rewrite !option_guard_True; set_solver.
-- 
GitLab