From 520faed9053baf7f29ab48ebcdf6614ee69b1a41 Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Mon, 17 Jan 2022 22:50:44 +0100
Subject: [PATCH] Bump gpfsl

---
 coq-lambda-rust.opam               | 2 +-
 theories/lang/arc.v                | 2 +-
 theories/lifetime/lifetime_sig.v   | 2 +-
 theories/lifetime/model/creation.v | 4 ++--
 theories/lifetime/model/faking.v   | 2 +-
 5 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index 7460dbef..54c7a4d4 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.2022-01-17.0.3e033cc4") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2022-01-17.1.eda41f52") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lang/arc.v b/theories/lang/arc.v
index d8b6b66e..2018feec 100644
--- a/theories/lang/arc.v
+++ b/theories/lang/arc.v
@@ -1523,7 +1523,7 @@ Section arc.
         rewrite decide_False; [done|by apply non_empty_singleton_L]. }
       iModIntro. iMod "Hclose1" as "_". iModIntro.
 
-      wp_case. iApply ("HΦ" with "[- $HP]"). iSplitL ""; [done|].
+      wp_case. iApply ("HΦ" with "[- $HP]").
       rewrite 2!monPred_objectively_elim. iFrame "HP1".
       iExists _,_,_, ∅. rewrite /StrongTok. iFrame "St'' tok'' R''".
       rewrite /StrMoves /StrDowns. iFrame "SM'' oW'' SD''".
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index 39fd08d5..a2d99b71 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -28,7 +28,7 @@ Module Type lifetime_sig.
   (** * Definitions *)
   Parameter lft : Type.
   Parameter static : lft.
-  Local Declare Instance lft_intersect : Meet lft.
+  Global Declare Instance lft_intersect : Meet lft.
 
   Section defs.
   Notation monPred Σ Lat := (monPredI (lat_bi_index Lat) (uPredI (iResUR Σ))).
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index 51ab71b8..63919e38 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -138,14 +138,14 @@ Proof.
     destruct (decide (κ1 = κ)) as [->|], (decide (κ2 = κ)) as [->|];
       rewrite ?functions.fn_lookup_insert ?functions.fn_lookup_insert_ne //.
     + destruct (Hκmin κ2) as [_ []]=>//. apply strict_spec_alt. auto.
-    + rewrite -lat_join_sqsubseteq_r.
+    + rewrite <-lat_join_sqsubseteq_r.
       assert (Hκ1K : κ1 ∈ elements (filter (κ ⊂.) K)).
       { apply elem_of_elements. rewrite elem_of_filter.
         split; [|done]. apply strict_spec_alt. auto. }
       clear -Hκ1K. induction Hκ1K; solve_lat.
     + apply Hmono=>//; rewrite elem_of_difference elem_of_singleton; auto.
   - rewrite (big_sepS_delete _ K) //. iSplitL "Hinv".
-    + by rewrite functions.fn_lookup_insert -lat_join_sqsubseteq_l.
+    + rewrite functions.fn_lookup_insert. by rewrite <-lat_join_sqsubseteq_l.
     + iApply (@big_sepS_impl with "[$HK]"). iModIntro. iIntros (κ').
       rewrite elem_of_difference elem_of_singleton. iIntros ([??]) "H".
         rewrite functions.fn_lookup_insert_ne //.
diff --git a/theories/lifetime/model/faking.v b/theories/lifetime/model/faking.v
index 334b4e96..37b488cc 100644
--- a/theories/lifetime/model/faking.v
+++ b/theories/lifetime/model/faking.v
@@ -109,7 +109,7 @@ Proof.
   - iExists (<[γ:=bot]> B), (P ∗ Pinh)%I. rewrite !fmap_insert. iNext. by iFrame.
   - iExists γ. iSplitL.
     + iDestruct (monPred_in_intro True%I with "[//]") as (V) "[? _]".
-      iExists bot. iFrame. by rewrite [bot]lat_bottom_sqsubseteq.
+      iExists bot. iFrame. by rewrite <-lat_bottom_sqsubseteq.
     + iExists P. iIntros "{$Hslice} !> !> **". by iApply (bi.iff_refl True%I).
 Qed.
 
-- 
GitLab