Move refcell into a folder.

_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

theories/typing/unsafe/ref.v → 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".

theories/typing/unsafe/refcell_code.v → 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.

theories/typing/unsafe/refmut.v → 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.