From 131651f14cc823889a0d73adefaaff5488c2c5cc Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Fri, 1 Oct 2021 12:05:21 +0200
Subject: [PATCH] bump gpfsl
---
coq-lambda-rust.opam | 2 +-
theories/lifetime/model/boxes.v | 3 ++-
theories/lifetime/model/definitions.v | 2 +-
3 files changed, 4 insertions(+), 3 deletions(-)
diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index 80244a85..29ca524b 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-09-27.0.77618673") | (= "dev") }
+ "coq-gpfsl" { (= "dev.2021-10-01.1.8da490e3") | (= "dev") }
]
build: [make "-j%{jobs}%"]
diff --git a/theories/lifetime/model/boxes.v b/theories/lifetime/model/boxes.v
index b3fdd23d..2772a22a 100644
--- a/theories/lifetime/model/boxes.v
+++ b/theories/lifetime/model/boxes.v
@@ -2,7 +2,8 @@ From iris.base_logic.lib Require Export invariants.
From iris.algebra Require Import auth gmap agree excl.
From iris.bi Require Import big_op.
From iris.proofmode Require Import tactics.
-From gpfsl.base_logic Require Import vprop lattice_cmra.
+From gpfsl.base_logic Require Import vprop.
+From gpfsl.algebra Require Import lattice_cmra.
Set Default Proof Using "Type".
Import uPred.
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index 7a4c5972..5913de4a 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -1,7 +1,7 @@
From iris.algebra Require Import csum auth excl frac gmap agree gset numbers.
From lrust.lifetime.model Require Import boxes.
From lrust.lifetime Require Export lifetime_sig.
-From gpfsl.base_logic Require Export lattice_cmra.
+From gpfsl.algebra Require Export lattice_cmra.
Set Default Proof Using "Type".
Import uPred.
Implicit Types (Lat : latticeT) (E : coPset).
--
GitLab