diff --git a/_CoqProject b/_CoqProject
index d7abc183f042ddceac4f23c633e1020a554c0d99..dc79c329b959f2b82a2f6d24ed24584928450c7c 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -32,11 +32,11 @@ theories/bi/big_op.v
 theories/bi/updates.v
 theories/bi/bi.v
 theories/bi/tactics.v
-theories/bi/fractional.v
 theories/bi/counter_examples.v
 theories/bi/fixpoint.v
 theories/bi/monpred.v
 theories/bi/embedding.v
+theories/bi/lib/fractional.v
 theories/base_logic/upred.v
 theories/base_logic/derived.v
 theories/base_logic/base_logic.v
diff --git a/theories/base_logic/lib/cancelable_invariants.v b/theories/base_logic/lib/cancelable_invariants.v
index 9d5f84d7fca628a905617733f9271e6ece09ce57..fa21aad639eed6efdb94f3b25e040d2f813405ad 100644
--- a/theories/base_logic/lib/cancelable_invariants.v
+++ b/theories/base_logic/lib/cancelable_invariants.v
@@ -1,5 +1,5 @@
 From iris.base_logic.lib Require Export invariants.
-From iris.bi Require Import fractional.
+From iris.bi.lib Require Import fractional.
 From iris.algebra Require Export frac.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index c37e3b6780f7456a7a85c06c72957bb20c7c513f..3550f0cd70dc86e69d55698209d7391b40150d40 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -1,6 +1,6 @@
 From iris.algebra Require Import auth gmap frac agree.
 From iris.base_logic.lib Require Export own.
-From iris.bi Require Import fractional.
+From iris.bi.lib Require Import fractional.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 Import uPred.
diff --git a/theories/bi/fractional.v b/theories/bi/lib/fractional.v
similarity index 100%
rename from theories/bi/fractional.v
rename to theories/bi/lib/fractional.v