From a77064a16472dcca106b0083ab965a27fbe88c21 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Wed, 25 Jan 2017 19:10:03 +0100
Subject: [PATCH] Move refcell into a folder.
---
_CoqProject | 8 ++++----
theories/typing/unsafe/{ => refcell}/ref.v | 3 ++-
theories/typing/unsafe/{ => refcell}/refcell.v | 0
theories/typing/unsafe/{ => refcell}/refcell_code.v | 2 +-
theories/typing/unsafe/{ => refcell}/refmut.v | 3 ++-
5 files changed, 9 insertions(+), 7 deletions(-)
rename theories/typing/unsafe/{ => refcell}/ref.v (98%)
rename theories/typing/unsafe/{ => refcell}/refcell.v (100%)
rename theories/typing/unsafe/{ => refcell}/refcell_code.v (99%)
rename theories/typing/unsafe/{ => refcell}/refmut.v (98%)
diff --git a/_CoqProject b/_CoqProject
index 3b46b5e5..d68db4dc 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 f84d53a2..3996978f 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 e0ffd902..130d5fc9 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 4b63921c..4076f850 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.
--
GitLab