From 3bb06eb84e5a66d8c1f7724d205d11594c7f9d84 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 6 Mar 2017 16:31:30 +0100
Subject: [PATCH] Move non-core typings into theories/typing/lib
---
_CoqProject | 32 +++++++++----------
theories/typing/{unsafe => lib}/cell.v | 0
.../typing/{unsafe => lib}/fake_shared_box.v | 0
theories/typing/{ => lib}/option.v | 0
theories/typing/{unsafe => lib}/refcell/ref.v | 2 +-
.../typing/{unsafe => lib}/refcell/ref_code.v | 2 +-
.../typing/{unsafe => lib}/refcell/refcell.v | 0
.../{unsafe => lib}/refcell/refcell_code.v | 2 +-
.../typing/{unsafe => lib}/refcell/refmut.v | 2 +-
.../{unsafe => lib}/refcell/refmut_code.v | 2 +-
.../typing/{unsafe => lib}/rwlock/rwlock.v | 0
.../{unsafe => lib}/rwlock/rwlock_code.v | 2 +-
.../{unsafe => lib}/rwlock/rwlockreadguard.v | 2 +-
.../rwlock/rwlockreadguard_code.v | 2 +-
.../{unsafe => lib}/rwlock/rwlockwriteguard.v | 2 +-
.../rwlock/rwlockwriteguard_code.v | 2 +-
theories/typing/{unsafe => lib}/spawn.v | 0
17 files changed, 26 insertions(+), 26 deletions(-)
rename theories/typing/{unsafe => lib}/cell.v (100%)
rename theories/typing/{unsafe => lib}/fake_shared_box.v (100%)
rename theories/typing/{ => lib}/option.v (100%)
rename theories/typing/{unsafe => lib}/refcell/ref.v (98%)
rename theories/typing/{unsafe => lib}/refcell/ref_code.v (99%)
rename theories/typing/{unsafe => lib}/refcell/refcell.v (100%)
rename theories/typing/{unsafe => lib}/refcell/refcell_code.v (99%)
rename theories/typing/{unsafe => lib}/refcell/refmut.v (99%)
rename theories/typing/{unsafe => lib}/refcell/refmut_code.v (99%)
rename theories/typing/{unsafe => lib}/rwlock/rwlock.v (100%)
rename theories/typing/{unsafe => lib}/rwlock/rwlock_code.v (99%)
rename theories/typing/{unsafe => lib}/rwlock/rwlockreadguard.v (98%)
rename theories/typing/{unsafe => lib}/rwlock/rwlockreadguard_code.v (99%)
rename theories/typing/{unsafe => lib}/rwlock/rwlockwriteguard.v (99%)
rename theories/typing/{unsafe => lib}/rwlock/rwlockwriteguard_code.v (99%)
rename theories/typing/{unsafe => lib}/spawn.v (100%)
diff --git a/_CoqProject b/_CoqProject
index c2110fe3..411cae53 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -45,22 +45,22 @@ theories/typing/fixpoint.v
theories/typing/type_sum.v
theories/typing/typing.v
theories/typing/soundness.v
-theories/typing/option.v
-theories/typing/unsafe/fake_shared_box.v
-theories/typing/unsafe/cell.v
-theories/typing/unsafe/spawn.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/refcell/ref_code.v
-theories/typing/unsafe/refcell/refmut_code.v
-theories/typing/unsafe/rwlock/rwlock.v
-theories/typing/unsafe/rwlock/rwlockreadguard.v
-theories/typing/unsafe/rwlock/rwlockwriteguard.v
-theories/typing/unsafe/rwlock/rwlock_code.v
-theories/typing/unsafe/rwlock/rwlockreadguard_code.v
-theories/typing/unsafe/rwlock/rwlockwriteguard_code.v
+theories/typing/lib/option.v
+theories/typing/lib/fake_shared_box.v
+theories/typing/lib/cell.v
+theories/typing/lib/spawn.v
+theories/typing/lib/refcell/refcell.v
+theories/typing/lib/refcell/ref.v
+theories/typing/lib/refcell/refmut.v
+theories/typing/lib/refcell/refcell_code.v
+theories/typing/lib/refcell/ref_code.v
+theories/typing/lib/refcell/refmut_code.v
+theories/typing/lib/rwlock/rwlock.v
+theories/typing/lib/rwlock/rwlockreadguard.v
+theories/typing/lib/rwlock/rwlockwriteguard.v
+theories/typing/lib/rwlock/rwlock_code.v
+theories/typing/lib/rwlock/rwlockreadguard_code.v
+theories/typing/lib/rwlock/rwlockwriteguard_code.v
theories/typing/examples/get_x.v
theories/typing/examples/rebor.v
theories/typing/examples/unbox.v
diff --git a/theories/typing/unsafe/cell.v b/theories/typing/lib/cell.v
similarity index 100%
rename from theories/typing/unsafe/cell.v
rename to theories/typing/lib/cell.v
diff --git a/theories/typing/unsafe/fake_shared_box.v b/theories/typing/lib/fake_shared_box.v
similarity index 100%
rename from theories/typing/unsafe/fake_shared_box.v
rename to theories/typing/lib/fake_shared_box.v
diff --git a/theories/typing/option.v b/theories/typing/lib/option.v
similarity index 100%
rename from theories/typing/option.v
rename to theories/typing/lib/option.v
diff --git a/theories/typing/unsafe/refcell/ref.v b/theories/typing/lib/refcell/ref.v
similarity index 98%
rename from theories/typing/unsafe/refcell/ref.v
rename to theories/typing/lib/refcell/ref.v
index c9c8b761..9fe6e746 100644
--- a/theories/typing/unsafe/refcell/ref.v
+++ b/theories/typing/lib/refcell/ref.v
@@ -3,7 +3,7 @@ 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.
-From lrust.typing.unsafe.refcell Require Import refcell.
+From lrust.typing.lib.refcell Require Import refcell.
Set Default Proof Using "Type".
Definition refcell_refN := refcellN .@ "ref".
diff --git a/theories/typing/unsafe/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
similarity index 99%
rename from theories/typing/unsafe/refcell/ref_code.v
rename to theories/typing/lib/refcell/ref_code.v
index 8028c93e..e2858d93 100644
--- a/theories/typing/unsafe/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -4,7 +4,7 @@ From iris.algebra Require Import auth csum frac agree.
From iris.base_logic Require Import big_op fractional.
From lrust.lifetime Require Import lifetime na_borrow.
From lrust.typing Require Import typing.
-From lrust.typing.unsafe.refcell Require Import refcell ref.
+From lrust.typing.lib.refcell Require Import refcell ref.
Set Default Proof Using "Type".
Section ref_functions.
diff --git a/theories/typing/unsafe/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
similarity index 100%
rename from theories/typing/unsafe/refcell/refcell.v
rename to theories/typing/lib/refcell/refcell.v
diff --git a/theories/typing/unsafe/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
similarity index 99%
rename from theories/typing/unsafe/refcell/refcell_code.v
rename to theories/typing/lib/refcell/refcell_code.v
index af0545bc..d807fb20 100644
--- a/theories/typing/unsafe/refcell/refcell_code.v
+++ b/theories/typing/lib/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 option.
-From lrust.typing.unsafe.refcell Require Import refcell ref refmut.
+From lrust.typing.lib.refcell Require Import refcell ref refmut.
Set Default Proof Using "Type".
Section refcell_functions.
diff --git a/theories/typing/unsafe/refcell/refmut.v b/theories/typing/lib/refcell/refmut.v
similarity index 99%
rename from theories/typing/unsafe/refcell/refmut.v
rename to theories/typing/lib/refcell/refmut.v
index 2dbaf846..bc9e076c 100644
--- a/theories/typing/unsafe/refcell/refmut.v
+++ b/theories/typing/lib/refcell/refmut.v
@@ -3,7 +3,7 @@ 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.
-From lrust.typing.unsafe.refcell Require Import refcell.
+From lrust.typing.lib.refcell Require Import refcell.
Set Default Proof Using "Type".
Section refmut.
diff --git a/theories/typing/unsafe/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
similarity index 99%
rename from theories/typing/unsafe/refcell/refmut_code.v
rename to theories/typing/lib/refcell/refmut_code.v
index d4b0c140..b0c55bed 100644
--- a/theories/typing/unsafe/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -4,7 +4,7 @@ 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.
-From lrust.typing.unsafe.refcell Require Import refcell refmut.
+From lrust.typing.lib.refcell Require Import refcell refmut.
Set Default Proof Using "Type".
Section refmut_functions.
diff --git a/theories/typing/unsafe/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
similarity index 100%
rename from theories/typing/unsafe/rwlock/rwlock.v
rename to theories/typing/lib/rwlock/rwlock.v
diff --git a/theories/typing/unsafe/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
similarity index 99%
rename from theories/typing/unsafe/rwlock/rwlock_code.v
rename to theories/typing/lib/rwlock/rwlock_code.v
index f077e072..bb3f0400 100644
--- a/theories/typing/unsafe/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_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 option.
-From lrust.typing.unsafe.rwlock Require Import rwlock rwlockreadguard rwlockwriteguard.
+From lrust.typing.lib.rwlock Require Import rwlock rwlockreadguard rwlockwriteguard.
Set Default Proof Using "Type".
Section rwlock_functions.
diff --git a/theories/typing/unsafe/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
similarity index 98%
rename from theories/typing/unsafe/rwlock/rwlockreadguard.v
rename to theories/typing/lib/rwlock/rwlockreadguard.v
index 01076b7a..6a61a4ad 100644
--- a/theories/typing/unsafe/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -3,7 +3,7 @@ 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.
-From lrust.typing.unsafe.rwlock Require Import rwlock.
+From lrust.typing.lib.rwlock Require Import rwlock.
Set Default Proof Using "Type".
Section rwlockreadguard.
diff --git a/theories/typing/unsafe/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
similarity index 99%
rename from theories/typing/unsafe/rwlock/rwlockreadguard_code.v
rename to theories/typing/lib/rwlock/rwlockreadguard_code.v
index 786d1abb..12ececef 100644
--- a/theories/typing/unsafe/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -4,7 +4,7 @@ From iris.algebra Require Import auth csum frac agree.
From iris.base_logic Require Import big_op fractional.
From lrust.lifetime Require Import lifetime na_borrow.
From lrust.typing Require Import typing.
-From lrust.typing.unsafe.rwlock Require Import rwlock rwlockreadguard.
+From lrust.typing.lib.rwlock Require Import rwlock rwlockreadguard.
Set Default Proof Using "Type".
Section rwlockreadguard_functions.
diff --git a/theories/typing/unsafe/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v
similarity index 99%
rename from theories/typing/unsafe/rwlock/rwlockwriteguard.v
rename to theories/typing/lib/rwlock/rwlockwriteguard.v
index 660d3fd9..ac839732 100644
--- a/theories/typing/unsafe/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -3,7 +3,7 @@ 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.
-From lrust.typing.unsafe.rwlock Require Import rwlock.
+From lrust.typing.lib.rwlock Require Import rwlock.
Set Default Proof Using "Type".
Section rwlockwriteguard.
diff --git a/theories/typing/unsafe/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
similarity index 99%
rename from theories/typing/unsafe/rwlock/rwlockwriteguard_code.v
rename to theories/typing/lib/rwlock/rwlockwriteguard_code.v
index 4cf42859..62077176 100644
--- a/theories/typing/unsafe/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -4,7 +4,7 @@ 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.
-From lrust.typing.unsafe.rwlock Require Import rwlock rwlockwriteguard.
+From lrust.typing.lib.rwlock Require Import rwlock rwlockwriteguard.
Set Default Proof Using "Type".
Section rwlockwriteguard_functions.
diff --git a/theories/typing/unsafe/spawn.v b/theories/typing/lib/spawn.v
similarity index 100%
rename from theories/typing/unsafe/spawn.v
rename to theories/typing/lib/spawn.v
--
GitLab