From e87b3f2d9d229a7bdc537c9386fb14dd2e0e5c50 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 7 Oct 2024 12:00:05 +0200
Subject: [PATCH] fix imports

---
 theories/lifetime/lifetime.v     | 2 +-
 theories/lifetime/lifetime_sig.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index 7a260b4e..9837dfe6 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -1,4 +1,4 @@
-From orc11 Require Export base.
+From gpfsl.orc11 Require Export base.
 Require Import iris.bi.lib.fractional.
 From lrust.lifetime Require Export lifetime_sig.
 From lrust.lifetime.model Require definitions primitive accessors faking borrow
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index 958cb00d..3508afe0 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -2,7 +2,7 @@ From stdpp Require Export gmultiset strings.
 From iris.algebra Require Import frac.
 From iris.base_logic.lib Require Export invariants.
 From iris.bi Require Import fractional.
-From orc11 Require Import base.
+From gpfsl.orc11 Require Import base.
 From gpfsl.base_logic Require Export vprop.
 
 From iris.proofmode Require Import proofmode.
-- 
GitLab