From d79d50f2b2b788ec81acd04d68e4c88032466231 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 16 Jan 2022 22:42:49 -0500
Subject: [PATCH] update dependencies, add missing Frame instances

---
 coq-lambda-rust.opam                | 2 +-
 theories/lifetime/lifetime_sig.v    | 9 +++++++--
 theories/lifetime/model/primitive.v | 5 +++++
 theories/typing/lft_contexts.v      | 5 +++++
 4 files changed, 18 insertions(+), 3 deletions(-)

diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index 013e4b85..7460dbef 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 9f141050..39fd08d5 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 71c6bc1e..8d2d064f 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 720b53d9..f0b1ce59 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.
-- 
GitLab