From 626dff3d7ba4974c686f770e125e06b008cc9b71 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 19 Sep 2019 20:45:44 +0200
Subject: [PATCH] Bump gpfsl.

---
 opam                                  | 2 +-
 theories/lifetime/lifetime_sig.v      | 4 ++--
 theories/lifetime/model/boxes.v       | 6 +++---
 theories/lifetime/model/creation.v    | 8 ++++----
 theories/lifetime/model/definitions.v | 2 +-
 theories/lifetime/model/primitive.v   | 4 ++--
 theories/typing/lft_contexts.v        | 2 +-
 7 files changed, 14 insertions(+), 14 deletions(-)

diff --git a/opam b/opam
index f4069b4c..f83032d2 100644
--- a/opam
+++ b/opam
@@ -10,5 +10,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
 depends: [
-  "coq-gpfsl" { (= "dev.2019-09-15.0.a4aa00fe") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2019-09-19.0.5c030976") | (= "dev") }
 ]
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index 8899796c..fcfba654 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -66,8 +66,8 @@ Module Type lifetime_sig.
 
   Global Declare Instance lft_intersect_comm : Comm (A:=lft) eq (⊓).
   Global Declare Instance lft_intersect_assoc : Assoc (A:=lft) eq (⊓).
-  Global Declare Instance lft_intersect_inj_1 (κ : lft) : Inj eq eq (κ ⊓).
-  Global Declare Instance lft_intersect_inj_2 (κ : lft) : Inj eq eq (⊓ κ).
+  Global Declare Instance lft_intersect_inj_1 (κ : lft) : Inj eq eq (κ ⊓.).
+  Global Declare Instance lft_intersect_inj_2 (κ : lft) : Inj eq eq (.⊓ κ).
   Global Declare Instance lft_intersect_left_id : LeftId eq static meet.
   Global Declare Instance lft_intersect_right_id : RightId eq static meet.
 
diff --git a/theories/lifetime/model/boxes.v b/theories/lifetime/model/boxes.v
index 31ab24ea..7cae15f0 100644
--- a/theories/lifetime/model/boxes.v
+++ b/theories/lifetime/model/boxes.v
@@ -12,7 +12,7 @@ Implicit Types Lat : latticeT.
 Class boxG Lat Σ :=
   boxG_inG :> inG Σ (prodR
     (authR (optionUR (exclR (optionO (latO Lat)))))
-    (optionR (agreeR (laterO (Lat -d> iPreProp Σ))))).
+    (optionR (agreeR (laterO (Lat -d> iPrePropO Σ))))).
 
 Definition boxΣ Lat : gFunctors := #[
    GFunctor (authR (optionUR (exclR (optionO (latO Lat)))) *
@@ -228,7 +228,7 @@ Qed.
 
 Lemma box_empty E f P V :
   ↑N ⊆ E →
-  map_Forall (λ _, from_option (⊑ V) False) f →
+  map_Forall (λ _, from_option (.⊑ V) False) f →
   box N f P ={E}=∗ ▷ P V ∗ box N (const None <$> f) P.
 Proof.
   iDestruct 1 as (Φ) "[#HeqP Hf]".
@@ -237,7 +237,7 @@ Proof.
       inv N (slice_inv γ (Φ γ)))%I with "[> Hf]" as "[HΦ ?]".
   { rewrite -big_sepM_sep -big_sepM_fupd. iApply (@big_sepM_impl with "[$Hf]").
     iAlways; iIntros (γ o ?) "(Hγ' & #HγΦ & #Hinv)".
-    assert (Ho : from_option (⊑ V) False o) by eauto.
+    assert (Ho : from_option (.⊑ V) False o) by eauto.
     destruct o as [V'|]=>//. rewrite -Ho.
     iInv N as (b) "[>Hγ HΦ]" "Hclose".
     iDestruct (box_own_auth_agree γ b (Some _) with "[-]") as %EQ; first by iFrame.
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index 3e186017..e4b23b6c 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -36,7 +36,7 @@ Proof.
   iMod (box_empty with "Hbox") as "[HP Hbox]"=>//; first set_solver.
   { intros i s. by rewrite lookup_fmap fmap_Some=>-[? [/HB [?[-> ?]] ->]] /=. }
   rewrite lft_vs_unfold; iDestruct "Hvs" as (Vκ n) "(% & Hcnt & Hvs)".
-  iDestruct (big_sepS_filter_acc (⊂ κ) _ _ (dom _ I) with "Halive")
+  iDestruct (big_sepS_filter_acc (.⊂ κ) _ _ (dom _ I) with "Halive")
     as "[Halive Halive']"; [by eauto|].
   iApply fupd_trans. iApply (fupd_mask_mono (↑borN ∪ E0)); [set_solver+|].
   iMod ("Hvs" $! I Vs with "[//] [//] [HI Halive Hbox Hbor] HP Hκ")
@@ -117,13 +117,13 @@ Proof.
   iDestruct "Hmono" as %Hmono.
   rewrite /lft_inv. iDestruct "Hinv" as (Vκ) "[Hhv Hinv]".
   iDestruct "Hhv" as %Hhv. iDestruct "Hhv0" as %Hhv0.
-  unshelve iExists (<[κ := Vκ ⊔ foldr (⊔) ε (Vs <$> elements (filter (κ ⊂) K))]>Vs);
+  unshelve iExists (<[κ := Vκ ⊔ foldr (⊔) ε (Vs <$> elements (filter (κ ⊂.) K))]>Vs);
     try apply _; [shelve..|].
   repeat iSplit.
   - iPureIntro. intros κ' Hκ'K Λ HΛ. destruct (decide (κ = κ')) as [<-|].
     + rewrite functions.fn_lookup_insert. specialize (Hhv Λ HΛ).
       destruct (A !! Λ) as [[b VΛ]|] eqn:EQVΛ=>//=. apply lat_join_lub; [done|].
-      assert (HFA : Forall (λ κ', Vs κ' ⊑ VΛ) (elements (filter (κ ⊂) K))).
+      assert (HFA : Forall (λ κ', Vs κ' ⊑ VΛ) (elements (filter (κ ⊂.) K))).
       { apply set_Forall_elements. intros κ'. rewrite elem_of_filter=>-[Hκκ' Hκ'K'].
         specialize (λ H, Hhv0 κ' H Λ). rewrite EQVΛ in Hhv0. apply Hhv0.
         - rewrite elem_of_difference elem_of_singleton. split; [done|intros ->].
@@ -138,7 +138,7 @@ Proof.
       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.
-      assert (Hκ1K : κ1 ∈ elements (filter (κ ⊂) K)).
+      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.
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index 812e2b6b..5fb4dde0 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -175,7 +175,7 @@ Section defs.
       ⎡lft_bor_dead κ ∗ own_cnt κ (● 0)%nat ∗ lft_inh κ (Some V) Pi⎤)%I.
 
   Definition lft_has_view (A : gmap atomic_lft (bool * Lat)) (κ : lft) (Vκ : Lat) :=
-    ∀ Λ : atomic_lft, Λ ∈ κ → from_option ((Vκ ⊑) ∘ snd) False (A !! Λ).
+    ∀ Λ : atomic_lft, Λ ∈ κ → from_option ((Vκ ⊑.) ∘ snd) False (A !! Λ).
   Definition lft_alive_in (A : gmap atomic_lft (bool * Lat)) (κ : lft) : Prop :=
     ∀ Λ : atomic_lft, Λ ∈ κ → fst <$> A !! Λ = Some true.
   Definition lft_dead_in (A : gmap atomic_lft (bool * Lat)) (κ : lft) : Prop :=
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 54f4253a..9e0a64e1 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -268,8 +268,8 @@ Instance lft_inhabited : Inhabited lft := _.
 Instance bor_idx_inhabited : Inhabited bor_idx := _.
 Instance lft_intersect_comm : Comm (A:=lft) eq (⊓) := _.
 Instance lft_intersect_assoc : Assoc (A:=lft) eq (⊓) := _.
-Instance lft_intersect_inj_1 κ : Inj eq eq (κ ⊓) := _.
-Instance lft_intersect_inj_2 κ : Inj eq eq (⊓ κ) := _.
+Instance lft_intersect_inj_1 κ : Inj eq eq (κ ⊓.) := _.
+Instance lft_intersect_inj_2 κ : Inj eq eq (.⊓ κ) := _.
 Instance lft_intersect_left_id : LeftId eq static (⊓) := _.
 Instance lft_intersect_right_id : RightId eq static (⊓) := _.
 
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index ce48ae79..9c695f63 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -51,7 +51,7 @@ Section lft_contexts.
     - iDestruct "H" as "[Hq Hq']".
       iDestruct "Hq" as (κ0) "(% & Hq & #?)".
       iDestruct "Hq'" as (κ0') "(% & Hq' & #?)". simpl in *. subst.
-      rewrite (inj ((lft_intersect_list κs) ⊓) κ0' κ0) //.
+      rewrite (inj ((lft_intersect_list κs) ⊓.) κ0' κ0) //.
       iExists κ0. by iFrame "∗#".
   Qed.
 
-- 
GitLab