update dependencies, add missing Frame instances

coq-lambda-rust.opam

@@ -15,7 +15,7 @@ This branch uses a proper weak memory model.
 """
 
 depends: [
-  "coq-gpfsl" { (= "dev.2021-12-06.1.197f500e") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2022-01-17.0.3e033cc4") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]

theories/lifetime/lifetime_sig.v

@@ -4,7 +4,9 @@ From iris.base_logic.lib Require Export invariants.
 From iris.bi Require Import fractional.
 From orc11 Require Import base.
 From gpfsl.base_logic Require Export vprop.
-Set Default Proof Using "Type".
+
+From iris.proofmode Require Import proofmode.
+From iris.prelude Require Import options.
 
 Definition lftN : namespace := nroot .@ "lft".
 
@@ -26,7 +28,7 @@ Module Type lifetime_sig.
   (** * Definitions *)
   Parameter lft : Type.
   Parameter static : lft.
-  Declare Instance lft_intersect : Meet lft.
+  Local Declare Instance lft_intersect : Meet lft.
 
   Section defs.
   Notation monPred Σ Lat := (monPredI (lat_bi_index Lat) (uPredI (iResUR Σ))).
@@ -108,6 +110,9 @@ Module Type lifetime_sig.
   Global Declare Instance lft_tok_fractional κ : Fractional (λ q, q.[κ])%I.
   Global Declare Instance lft_tok_as_fractional κ q :
     AsFractional q.[κ] (λ q, q.[κ])%I q.
+  Global Declare Instance frame_lft_tok p κ q1 q2 RES :
+    FrameFractionalHyps p q1.[κ] (λ q, q.[κ])%I RES q1 q2 →
+    Frame p q1.[κ] q2.[κ] RES | 5.
 
   Global Declare Instance positive_to_lft_inj : Inj eq eq positive_to_lft.
 

theories/lifetime/model/primitive.v

@@ -325,6 +325,11 @@ Qed.
 Global Instance lft_tok_as_fractional κ q :
   AsFractional (q.[κ]) (λ q, q.[κ])%I q.
 Proof. split. done. apply _. Qed.
+Global Instance frame_lft_tok p κ q1 q2 RES :
+  FrameFractionalHyps p q1.[κ] (λ q, q.[κ])%I RES q1 q2 →
+  Frame p q1.[κ] q2.[κ] RES | 5.
+Proof. apply: frame_fractional. Qed.
+
 Lemma lft_tok_split_obj `{LatBottom Lat bot} q1 q2 κ :
   (q1 + q2).[κ] -∗ q1.[κ] ∗ <obj> q2.[κ].
 Proof.

theories/typing/lft_contexts.v

@@ -96,6 +96,11 @@ Section lft_contexts.
   Global Instance llctx_interp_as_fractional qmax L q :
     AsFractional (llctx_interp_noend qmax L q) (llctx_interp_noend qmax L) q.
   Proof. split; first done. apply _. Qed.
+  Global Instance frame_llctx_interp p qmax L q1 q2 RES :
+    FrameFractionalHyps p (llctx_interp_noend qmax L q1) (llctx_interp_noend qmax L) RES q1 q2 →
+    Frame p (llctx_interp_noend qmax L q1) (llctx_interp_noend qmax L q2) RES | 5.
+  Proof. apply: frame_fractional. Qed.
+
   Global Instance llctx_interp_permut qmax :
     Proper ((≡ₚ) ==> (⊣⊢)) (llctx_interp qmax).
   Proof. intros ???. by apply big_opL_permutation. Qed.