From 761dd4f32dbe8abf783db36390306be61e6eff66 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 3 Jun 2021 18:29:58 +0200
Subject: [PATCH] update dependencies

---
 coq-lambda-rust.opam                   |  2 +-
 theories/lifetime/at_borrow.v          |  4 ++--
 theories/lifetime/frac_borrow.v        |  6 +++---
 theories/lifetime/lifetime.v           |  2 +-
 theories/lifetime/lifetime_sig.v       | 14 +++++++-------
 theories/lifetime/meta.v               |  2 +-
 theories/lifetime/model/accessors.v    |  2 +-
 theories/lifetime/model/borrow.v       |  2 +-
 theories/lifetime/model/borrow_sep.v   |  2 +-
 theories/lifetime/model/boxes.v        |  4 ++--
 theories/lifetime/model/creation.v     |  2 +-
 theories/lifetime/model/definitions.v  |  4 ++--
 theories/lifetime/model/faking.v       |  2 +-
 theories/lifetime/model/in_at_borrow.v |  4 ++--
 theories/lifetime/model/primitive.v    |  4 ++--
 theories/lifetime/model/reborrow.v     |  2 +-
 theories/lifetime/na_borrow.v          |  4 ++--
 theories/typing/lft_contexts.v         |  4 ++--
 18 files changed, 33 insertions(+), 33 deletions(-)

diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index 0344def4..03d19f97 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-05-27.0.193d6230") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2021-06-03.0.d0c552b5") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lifetime/at_borrow.v b/theories/lifetime/at_borrow.v
index 3513d994..e0d685a2 100644
--- a/theories/lifetime/at_borrow.v
+++ b/theories/lifetime/at_borrow.v
@@ -9,12 +9,12 @@ Set Default Proof Using "Type".
    created, and the payload could be weakened without synchronizing
    with the end of the lifetime (remember that the underlying payload
    is not necessarily independent of the view for views older than V). *)
-Definition at_bor `{!invG Σ, !lftG Σ Lat userE} κ N (P : monPred _ _) : monPred _ _ :=
+Definition at_bor `{!invGS Σ, !lftG Σ Lat userE} κ N (P : monPred _ _) : monPred _ _ :=
   (∃ i, ⌜N ## lftN⌝ ∗ &{κ,i}P ∗ ⎡inv N (∃ V', idx_bor_own i V')⎤)%I.
 Notation "&at{ κ , N }" := (at_bor κ N) (format "&at{ κ , N }") : bi_scope.
 
 Section atomic_bors.
-  Context `{!invG Σ, !lftG Σ Lat userE}.
+  Context `{!invGS Σ, !lftG Σ Lat userE}.
 
   Global Instance at_bor_ne κ n N : Proper (dist n ==> dist n) (at_bor κ N).
   Proof. solve_proper. Qed.
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index 6c112d31..997b4a72 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -6,7 +6,7 @@ Set Default Proof Using "Type".
 
 Class frac_borG Σ := frac_borG_inG :> inG Σ fracR.
 
-Local Definition frac_bor_inv `{!invG Σ, !lftG Σ Lat userE, !frac_borG Σ}
+Local Definition frac_bor_inv `{!invGS Σ, !lftG Σ Lat userE, !frac_borG Σ}
                               (φ : Qp → monPred _ _) (V0 : Lat ) γ κ : monPred _ _:=
   (∃ (qfresh : Qp) (qdep qused : option Qp),
       (* We divide the 1 fraction into 3 parts... *)
@@ -24,7 +24,7 @@ Local Definition frac_bor_inv `{!invG Σ, !lftG Σ Lat userE, !frac_borG Σ}
          enough fractions of the lifetime in deposit. *)
       ⎡own γ (qfresh ⋅? qused)⎤)%I.
 
-Definition frac_bor `{!invG Σ, !lftG Σ Lat userE, !frac_borG Σ} κ
+Definition frac_bor `{!invGS Σ, !lftG Σ Lat userE, !frac_borG Σ} κ
         (φ : Qp → monPred _ _) : monPred _ _ :=
   (* First, we close up to a bunch of things: iff, lifetime inclusion and view
      inclusion. We also existentially bind γ, the ghost name of receipts. *)
@@ -38,7 +38,7 @@ Definition frac_bor `{!invG Σ, !lftG Σ Lat userE, !frac_borG Σ} κ
 Notation "&frac{ κ }" := (frac_bor κ) (format "&frac{ κ }") : bi_scope.
 
 Section frac_bor.
-  Context `{!invG Σ, !lftG Σ Lat userE, !frac_borG Σ}.
+  Context `{!invGS Σ, !lftG Σ Lat userE, !frac_borG Σ}.
   Implicit Types E : coPset.
 
   Global Instance frac_bor_contractive κ n :
diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index 3ca7be4b..e77f22f6 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -29,7 +29,7 @@ Definition lft_incl_syntactic (κ κ' : lft) : Prop := ∃ κ'', κ'' ⊓ κ' =
 Infix "⊑ˢʸⁿ" := lft_incl_syntactic (at level 40) : stdpp_scope.
 
 Section derived.
-Context `{!invG Σ, !lftG Σ Lat userE}.
+Context `{!invGS Σ, !lftG Σ Lat userE}.
 Implicit Types κ : lft.
 
 Lemma lft_create E `{LatBottom Lat} :
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index 04373ae2..9f141050 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -31,24 +31,24 @@ Module Type lifetime_sig.
   Section defs.
   Notation monPred Σ Lat := (monPredI (lat_bi_index Lat) (uPredI (iResUR Σ))).
 
-  Parameter lft_ctx : ∀ `{!invG Σ, !lftG Σ Lat userE}, iProp Σ.
+  Parameter lft_ctx : ∀ `{!invGS Σ, !lftG Σ Lat userE}, iProp Σ.
 
   Parameter lft_tok : ∀ `{!lftG Σ Lat userE} (q : Qp) (κ : lft), monPred Σ Lat.
   Parameter lft_dead : ∀ `{!lftG Σ Lat userE} (κ : lft), monPred Σ Lat.
 
   Parameter lft_incl :
-    ∀ `{!invG Σ, !lftG Σ Lat userE} (κ κ' : lft), monPred Σ Lat.
+    ∀ `{!invGS Σ, !lftG Σ Lat userE} (κ κ' : lft), monPred Σ Lat.
   Parameter bor :
-    ∀ `{!invG Σ, !lftG Σ Lat userE} (κ : lft) (P : monPred Σ Lat), monPred Σ Lat.
+    ∀ `{!invGS Σ, !lftG Σ Lat userE} (κ : lft) (P : monPred Σ Lat), monPred Σ Lat.
 
   Parameter bor_idx : Type.
   Parameter idx_bor_own : ∀ `{!lftG Σ Lat userE} (i : bor_idx), monPred Σ Lat.
   Parameter idx_bor :
-    ∀ `{!invG Σ, !lftG Σ Lat userE} (κ : lft) (i : bor_idx) (P : monPred Σ Lat),
+    ∀ `{!invGS Σ, !lftG Σ Lat userE} (κ : lft) (i : bor_idx) (P : monPred Σ Lat),
       monPred Σ Lat.
 
   Parameter in_at_bor :
-    ∀ `{!invG Σ, !lftG Σ Lat userE} (κ : lft) (P : monPred Σ Lat), monPred Σ Lat.
+    ∀ `{!invGS Σ, !lftG Σ Lat userE} (κ : lft) (P : monPred Σ Lat), monPred Σ Lat.
   End defs.
 
   (** Our lifetime creation lemma offers allocating a lifetime that is defined
@@ -68,7 +68,7 @@ Module Type lifetime_sig.
   Infix "⊑" := lft_incl (at level 70) : bi_scope.
 
   Section properties.
-  Context `{!invG Σ, !lftG Σ Lat userE}.
+  Context `{!invGS Σ, !lftG Σ Lat userE}.
 
   (** * Instances *)
   Global Declare Instance lft_inhabited : Inhabited lft.
@@ -224,7 +224,7 @@ Module Type lifetime_sig.
   Parameter lftΣ : latticeT → gFunctors.
   Global Declare Instance subG_lftPreG Lat Σ : subG (lftΣ Lat) Σ → lftPreG Σ Lat.
 
-  Parameter lft_init : ∀ `{!invG Σ, !lftPreG Σ Lat} E userE,
+  Parameter lft_init : ∀ `{!invGS Σ, !lftPreG Σ Lat} E userE,
       ↑lftN ⊆ E → ↑lftN ## userE →
       ⊢ |={E}=> ∃ _ : lftG Σ Lat userE, lft_ctx.
 End lifetime_sig.
diff --git a/theories/lifetime/meta.v b/theories/lifetime/meta.v
index f6d677a6..331d3cf2 100644
--- a/theories/lifetime/meta.v
+++ b/theories/lifetime/meta.v
@@ -26,7 +26,7 @@ Definition lft_meta `{!lftG Σ Lat userE, lft_metaG Σ} (κ : lft) (γ : gname)
     own lft_meta_gname (dyn_reservation_map_data p (to_agree γ)).
 
 Section lft_meta.
-  Context `{!invG Σ, !lftG Σ Lat userE, lft_metaG Σ}.
+  Context `{!invGS Σ, !lftG Σ Lat userE, lft_metaG Σ}.
 
   Global Instance lft_meta_timeless κ γ : Timeless (lft_meta κ γ).
   Proof. apply _. Qed.
diff --git a/theories/lifetime/model/accessors.v b/theories/lifetime/model/accessors.v
index 8f60ff19..234e65f1 100644
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -4,7 +4,7 @@ From iris.algebra Require Import csum auth excl frac gmap agree gset.
 Set Default Proof Using "Type".
 
 Section accessors.
-Context `{!invG Σ, !lftG Σ Lat userE}.
+Context `{!invGS Σ, !lftG Σ Lat userE}.
 Implicit Types κ : lft.
 
 (* Internal helper lemmas *)
diff --git a/theories/lifetime/model/borrow.v b/theories/lifetime/model/borrow.v
index 9b10f6b5..3c491d1c 100644
--- a/theories/lifetime/model/borrow.v
+++ b/theories/lifetime/model/borrow.v
@@ -5,7 +5,7 @@ From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type*".
 
 Section borrow.
-Context `{!invG Σ, !lftG Σ Lat userE, LatBottom Lat}.
+Context `{!invGS Σ, !lftG Σ Lat userE, LatBottom Lat}.
 Implicit Types κ : lft.
 
 Lemma raw_bor_create E κ P :
diff --git a/theories/lifetime/model/borrow_sep.v b/theories/lifetime/model/borrow_sep.v
index ef7f0cd1..8b7f5ced 100644
--- a/theories/lifetime/model/borrow_sep.v
+++ b/theories/lifetime/model/borrow_sep.v
@@ -28,7 +28,7 @@ Proof.
 Qed.
 
 Section borrow.
-Context `{!invG Σ, !lftG Σ Lat userE, LatBottom Lat}.
+Context `{!invGS Σ, !lftG Σ Lat userE, LatBottom Lat}.
 Implicit Types κ : lft.
 
 Lemma bor_sep E κ P Q :
diff --git a/theories/lifetime/model/boxes.v b/theories/lifetime/model/boxes.v
index aaffe540..548df8b3 100644
--- a/theories/lifetime/model/boxes.v
+++ b/theories/lifetime/model/boxes.v
@@ -22,7 +22,7 @@ Instance subG_stsΣ Lat Σ : subG (boxΣ Lat) Σ → boxG Lat Σ.
 Proof. solve_inG. Qed.
 
 Section box_defs.
-  Context `{invG Σ, boxG Lat Σ} (N : namespace).
+  Context `{invGS Σ, boxG Lat Σ} (N : namespace).
   Notation iProp := (iProp Σ).
   Notation monPred := (monPred (lat_bi_index Lat) (uPredI (iResUR Σ))).
 
@@ -54,7 +54,7 @@ Instance: Params (@slice) 6 := {}.
 Instance: Params (@box) 6 := {}.
 
 Section box.
-Context `{invG Σ, boxG Lat Σ} (N : namespace).
+Context `{invGS Σ, boxG Lat Σ} (N : namespace).
 
 Notation monPred := (monPred (lat_bi_index Lat) (uPredI (iResUR Σ))).
 Implicit Types P Q : monPred.
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index d228d2ad..d4ed860e 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -5,7 +5,7 @@ From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type*".
 
 Section creation.
-Context `{!invG Σ, !lftG Σ Lat userE, LatBottom Lat}.
+Context `{!invGS Σ, !lftG Σ Lat userE, LatBottom Lat}.
 Implicit Types κ : lft.
 
 Lemma lft_kill (I : gmap lft lft_names) (K K' : gset lft) (κ : lft) (Vs : lft → Lat) :
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index 31feccb7..7a4c5972 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -84,7 +84,7 @@ Definition to_borUR {Lat} : gmap slice_name (bor_state Lat) → borUR Lat :=
   fmap Excl.
 
 Section defs.
-  Context `{!invG Σ, !lftG Σ Lat userE}.
+  Context `{!invGS Σ, !lftG Σ Lat userE}.
 
   Notation iProp := (iProp Σ).
   Notation monPred := (monPred (lat_bi_index Lat) (uPredI (iResUR Σ))).
@@ -236,7 +236,7 @@ Typeclasses Opaque lft_tok lft_dead bor_cnt lft_bor_alive lft_bor_dead
   idx_bor_own idx_bor raw_bor bor.
 
 Section basic_properties.
-Context `{!invG Σ, !lftG Σ Lat userE}.
+Context `{!invGS Σ, !lftG Σ Lat userE}.
 Implicit Types κ : lft.
 
 Notation iProp := (iProp Σ).
diff --git a/theories/lifetime/model/faking.v b/theories/lifetime/model/faking.v
index cb4d43b1..334b4e96 100644
--- a/theories/lifetime/model/faking.v
+++ b/theories/lifetime/model/faking.v
@@ -4,7 +4,7 @@ From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type*".
 
 Section faking.
-Context `{!invG Σ, !lftG Σ Lat userE, LatBottom Lat bot}.
+Context `{!invGS Σ, !lftG Σ Lat userE, LatBottom Lat bot}.
 Implicit Types κ : lft.
 
 Lemma ilft_create A I κ :
diff --git a/theories/lifetime/model/in_at_borrow.v b/theories/lifetime/model/in_at_borrow.v
index a3459a39..a7677e2e 100644
--- a/theories/lifetime/model/in_at_borrow.v
+++ b/theories/lifetime/model/in_at_borrow.v
@@ -16,7 +16,7 @@ Set Default Proof Using "Type".
 
 Definition in_atN : namespace := lftN .@ "in_at".
 
-Definition in_at_bor `{invG Σ, lftG Σ Lat userE} κ P :=
+Definition in_at_bor `{invGS Σ, lftG Σ Lat userE} κ P :=
     (∃ P' i, (κ ⊑ (i.1))
                ∗ ▷ □ (P' ↔ P) ∗ ⎡slice borN (i.2) P'⎤
                ∗ ⎡inv in_atN (∃ V', idx_bor_own i V')⎤)%I.
@@ -24,7 +24,7 @@ Notation "&in_at{ κ }" := (in_at_bor κ) (format "&in_at{ κ }") : bi_scope.
 Instance in_at_bor_params : Params (@in_at_bor) 5 := {}.
 
 Section in_at.
-Context `{invG Σ, lftG Σ Lat userE}.
+Context `{invGS Σ, lftG Σ Lat userE}.
 
 Global Instance in_at_bor_ne κ n : Proper (dist n ==> dist n) (in_at_bor κ).
 Proof. solve_proper. Qed.
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 1e54efe6..71c6bc1e 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -5,7 +5,7 @@ From lrust.lifetime.model Require Export definitions boxes.
 Set Default Proof Using "Type".
 Import uPred.
 
-Lemma lft_init `{!invG Σ, !lftPreG Σ Lat} E userE :
+Lemma lft_init `{!invGS Σ, !lftPreG Σ Lat} E userE :
   ↑lftN ⊆ E → ↑lftN ## userE → ⊢ |={E}=> ∃ _ : lftG Σ Lat userE, lft_ctx.
 Proof.
   iIntros (? HuserE). rewrite /lft_ctx.
@@ -19,7 +19,7 @@ Proof.
 Qed.
 
 Section primitive.
-Context `{!invG Σ, !lftG Σ Lat userE}.
+Context `{!invGS Σ, !lftG Σ Lat userE}.
 Implicit Types κ : lft.
 
 Lemma to_borUR_included (B : gmap slice_name (bor_state Lat)) i s :
diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v
index 6a20e460..9bda0563 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -29,7 +29,7 @@ Proof.
 Qed.
 
 Section reborrow.
-Context `{!invG Σ, !lftG Σ Lat userE, LatBottom Lat}.
+Context `{!invGS Σ, !lftG Σ Lat userE, LatBottom Lat}.
 Implicit Types κ : lft.
 
 (* Notice that taking lft_inv for both κ and κ' already implies
diff --git a/theories/lifetime/na_borrow.v b/theories/lifetime/na_borrow.v
index bf16113d..a5ed5cd9 100644
--- a/theories/lifetime/na_borrow.v
+++ b/theories/lifetime/na_borrow.v
@@ -3,7 +3,7 @@ From gpfsl.logic Require Export na_invariants.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
-Definition na_bor `{!invG Σ, !lftG Σ View userE, na_invG View bot Σ}
+Definition na_bor `{!invGS Σ, !lftG Σ View userE, na_invG View bot Σ}
            (κ : lft) (tid : na_inv_pool_name) (N : namespace) (P : monPred _ _) :=
   (∃ i, &{κ,i}P ∗ na_inv tid N (idx_bor_own i))%I.
 
@@ -11,7 +11,7 @@ Notation "&na{ κ , tid , N }" := (na_bor κ tid N)
     (format "&na{ κ , tid , N }") : bi_scope.
 
 Section na_bor.
-  Context `{!invG Σ, !lftG Σ View userE, na_invG View bot Σ}
+  Context `{!invGS Σ, !lftG Σ View userE, na_invG View bot Σ}
           (tid : na_inv_pool_name) (N : namespace).
 
   Global Instance na_bor_ne κ n : Proper (dist n ==> dist n) (na_bor κ tid N).
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 03f38776..720b53d9 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -23,7 +23,7 @@ Notation llctx := (list llctx_elt).
 Notation "κ ⊑ₗ κl" := (@pair lft (list lft) κ κl) (at level 70).
 
 Section lft_contexts.
-  Context `{!invG Σ, !lftG Σ view_Lat lft_userE}.
+  Context `{!invGS Σ, !lftG Σ view_Lat lft_userE}.
   Implicit Type (κ : lft).
 
   (* External lifetime contexts. *)
@@ -415,7 +415,7 @@ Arguments lctx_lft_incl_incl_noend {_ _ _ _} _ _.
 Arguments lctx_lft_alive_tok {_ _ _ _ _} _ _ _.
 Arguments lctx_lft_alive_tok_noend {_ _ _ _ _} _ _ _.
 
-Lemma elctx_sat_submseteq `{!invG Σ, !lftG Σ view_Lat lft_userE} E E' L :
+Lemma elctx_sat_submseteq `{!invGS Σ, !lftG Σ view_Lat lft_userE} E E' L :
   E' ⊆+ E → elctx_sat E L E'.
 Proof. iIntros (HE' ??) "_ !> H". by iApply big_sepL_submseteq. Qed.
 
-- 
GitLab