From 943d7adc7a59fcde48fc163f67c6c3513094a8c0 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 30 Mar 2017 17:45:05 +0200
Subject: [PATCH] Move some things from lang/ to lang/lib/
---
_CoqProject | 6 +++---
theories/lang/{ => lib}/memcpy.v | 0
theories/lang/{ => lib}/new_delete.v | 0
theories/lang/{ => lib}/spawn.v | 0
theories/typing/lib/cell.v | 2 +-
theories/typing/lib/rc.v | 2 +-
theories/typing/lib/refcell/refcell_code.v | 2 +-
theories/typing/lib/rwlock/rwlock_code.v | 2 +-
theories/typing/own.v | 3 +--
9 files changed, 8 insertions(+), 9 deletions(-)
rename theories/lang/{ => lib}/memcpy.v (100%)
rename theories/lang/{ => lib}/new_delete.v (100%)
rename theories/lang/{ => lib}/spawn.v (100%)
diff --git a/_CoqProject b/_CoqProject
index 5cd928c7..7f6a715d 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -17,13 +17,13 @@ theories/lang/adequacy.v
theories/lang/heap.v
theories/lang/lang.v
theories/lang/lifting.v
-theories/lang/memcpy.v
-theories/lang/new_delete.v
theories/lang/notation.v
theories/lang/proofmode.v
theories/lang/races.v
theories/lang/tactics.v
-theories/lang/spawn.v
+theories/lang/lib/memcpy.v
+theories/lang/lib/new_delete.v
+theories/lang/lib/spawn.v
theories/typing/base.v
theories/typing/type.v
theories/typing/util.v
diff --git a/theories/lang/memcpy.v b/theories/lang/lib/memcpy.v
similarity index 100%
rename from theories/lang/memcpy.v
rename to theories/lang/lib/memcpy.v
diff --git a/theories/lang/new_delete.v b/theories/lang/lib/new_delete.v
similarity index 100%
rename from theories/lang/new_delete.v
rename to theories/lang/lib/new_delete.v
diff --git a/theories/lang/spawn.v b/theories/lang/lib/spawn.v
similarity index 100%
rename from theories/lang/spawn.v
rename to theories/lang/lib/spawn.v
diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index 023d116b..9234d7f8 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -1,6 +1,6 @@
From iris.proofmode Require Import tactics.
From iris.base_logic Require Import big_op.
-From lrust.lang Require Import memcpy.
+From lrust.lang.lib Require Import memcpy.
From lrust.lifetime Require Import na_borrow.
From lrust.typing Require Export type.
From lrust.typing Require Import typing.
diff --git a/theories/typing/lib/rc.v b/theories/typing/lib/rc.v
index 4f67aa13..a3ede2cf 100644
--- a/theories/typing/lib/rc.v
+++ b/theories/typing/lib/rc.v
@@ -2,7 +2,7 @@ From Coq.QArith Require Import Qcanon.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import auth csum frac agree.
From iris.base_logic Require Import big_op.
-From lrust.lang Require Import memcpy.
+From lrust.lang.lib Require Import memcpy.
From lrust.lifetime Require Import na_borrow.
From lrust.typing Require Export type.
From lrust.typing Require Import typing option.
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index fcea5370..b68b7e89 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -2,7 +2,7 @@ From Coq.QArith Require Import Qcanon.
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.lang Require Import memcpy.
+From lrust.lang.lib Require Import memcpy.
From lrust.lifetime Require Import na_borrow.
From lrust.typing Require Import typing option.
From lrust.typing.lib.refcell Require Import refcell ref refmut.
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index a82f950b..1d81abac 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -2,7 +2,7 @@ From Coq.QArith Require Import Qcanon.
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.lang Require Import memcpy.
+From lrust.lang.lib Require Import memcpy.
From lrust.lifetime Require Import na_borrow.
From lrust.typing Require Import typing option.
From lrust.typing.lib.rwlock Require Import rwlock rwlockreadguard rwlockwriteguard.
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 5268ca38..f023f1e4 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -1,8 +1,7 @@
From Coq Require Import Qcanon.
From iris.proofmode Require Import tactics.
From iris.base_logic Require Import big_op.
-From lrust.lang Require Export new_delete.
-From lrust.lang Require Import memcpy.
+From lrust.lang.lib Require Import new_delete memcpy.
From lrust.typing Require Export type.
From lrust.typing Require Import util uninit type_context programs.
Set Default Proof Using "Type".
--
GitLab