Bump.

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

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.