diff --git a/_CoqProject b/_CoqProject
index 3b46b5e53d7645358ae070139911d6ce455894a3..d68db4dcc7ec2e8edcb892a419486061f421ea1b 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -52,7 +52,7 @@ theories/typing/examples/option_as_mut.v
 theories/typing/examples/unwrap_or.v
 theories/typing/examples/lazy_lft.v
 theories/typing/unsafe/cell.v
-theories/typing/unsafe/refcell.v
-theories/typing/unsafe/ref.v
-theories/typing/unsafe/refmut.v
-theories/typing/unsafe/refcell_code.v
+theories/typing/unsafe/refcell/refcell.v
+theories/typing/unsafe/refcell/ref.v
+theories/typing/unsafe/refcell/refmut.v
+theories/typing/unsafe/refcell/refcell_code.v
diff --git a/theories/typing/unsafe/ref.v b/theories/typing/unsafe/refcell/ref.v
similarity index 98%
rename from theories/typing/unsafe/ref.v
rename to theories/typing/unsafe/refcell/ref.v
index f84d53a29e8a3469dfa363b868032867d2a19be3..3996978fa8a94533e0feef206665f1ccf5ea0c2c 100644
--- a/theories/typing/unsafe/ref.v
+++ b/theories/typing/unsafe/refcell/ref.v
@@ -2,7 +2,8 @@ From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth csum frac agree.
 From iris.base_logic Require Import big_op fractional.
 From lrust.lifetime Require Import na_borrow.
-From lrust.typing Require Import typing refcell.
+From lrust.typing Require Import typing.
+From lrust.typing.unsafe.refcell Require Import refcell.
 Set Default Proof Using "Type".
 
 Definition refcell_refN := refcellN .@ "ref".
diff --git a/theories/typing/unsafe/refcell.v b/theories/typing/unsafe/refcell/refcell.v
similarity index 100%
rename from theories/typing/unsafe/refcell.v
rename to theories/typing/unsafe/refcell/refcell.v
diff --git a/theories/typing/unsafe/refcell_code.v b/theories/typing/unsafe/refcell/refcell_code.v
similarity index 99%
rename from theories/typing/unsafe/refcell_code.v
rename to theories/typing/unsafe/refcell/refcell_code.v
index e0ffd902e4050eda8a294162ac0b24ab2ba5ede6..130d5fc9997d5c5d2358231d7dd60f98f8ae8839 100644
--- a/theories/typing/unsafe/refcell_code.v
+++ b/theories/typing/unsafe/refcell/refcell_code.v
@@ -5,7 +5,7 @@ From iris.base_logic Require Import big_op fractional.
 From lrust.lang Require Import memcpy.
 From lrust.lifetime Require Import na_borrow.
 From lrust.typing Require Import typing.
-From lrust.typing.unsafe Require Import refcell ref refmut.
+From lrust.typing.unsafe.refcell Require Import refcell ref refmut.
 Set Default Proof Using "Type".
 
 Section refcell_functions.
diff --git a/theories/typing/unsafe/refmut.v b/theories/typing/unsafe/refcell/refmut.v
similarity index 98%
rename from theories/typing/unsafe/refmut.v
rename to theories/typing/unsafe/refcell/refmut.v
index 4b63921c54863b45d2ad560af2028e6b59037a5a..4076f85019fc904ba526bec8da02589fa0ab3627 100644
--- a/theories/typing/unsafe/refmut.v
+++ b/theories/typing/unsafe/refcell/refmut.v
@@ -2,7 +2,8 @@ From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth csum frac agree.
 From iris.base_logic Require Import big_op fractional.
 From lrust.lifetime Require Import na_borrow.
-From lrust.typing Require Import typing refcell.
+From lrust.typing Require Import typing.
+From lrust.typing.unsafe.refcell Require Import refcell.
 Set Default Proof Using "Type".
 
 Section refmut.