diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index 013e4b85d771863c2253a8159e5391494d6f1071..7460dbef8eec073aab127068af6adc50e4035e29 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-12-06.1.197f500e") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2022-01-17.0.3e033cc4") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index 9f1410507b1e2bdcc2352076170ec67852115d11..39fd08d52265103ecbf3f3101633129f4bfc1ddb 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/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.
 
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 71c6bc1e6836b5e1e067e73f690bd0e9e674a977..8d2d064f34855b3ec81dd9c41b1021a0f5d853c0 100644
--- a/theories/lifetime/model/primitive.v
+++ b/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.
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 720b53d9143a4663ad44c247df4e425e6f917416..f0b1ce590d63d3675a3bcb8be2c40059b18c12aa 100644
--- a/theories/typing/lft_contexts.v
+++ b/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.