diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v index 7a260b4e26cebc1d45802c0ed63a68424827df77..9837dfe69e5ff8f81086cdd3a339eebf9c15d853 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 958cb00dc95e8e0d9e659679ba166b3db26a4f6a..3508afe0d8ef55c00f88f462f741144fabb2e257 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.