diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index 80244a85afcd96ff6aae2dfa89769e43c9f7cf28..29ca524bb16ba08e7cb045294bf101960c5810ce 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 b3fdd23d65037b85e6d2318bc82e23cf8926301a..2772a22a9e29e89db938f51c3d5379438c6b0eac 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 7a4c5972bf6d22b230faa4baf0ec6884fe305186..5913de4abe9bffa63954fe86eaff1a5630b995b6 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).