From a25d9f574e84ec5ce6d980ad6b7be6921217b42d Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jjourdan@mpi-sws.org>
Date: Wed, 11 Jan 2017 18:49:47 +0100
Subject: [PATCH] I can't make a commit with a new file without forgetting to
 add it...

---
 theories/typing/typing.v | 9 +++++++++
 1 file changed, 9 insertions(+)
 create mode 100644 theories/typing/typing.v

diff --git a/theories/typing/typing.v b/theories/typing/typing.v
new file mode 100644
index 00000000..cdbc2552
--- /dev/null
+++ b/theories/typing/typing.v
@@ -0,0 +1,9 @@
+From lrust.lang Require Export tactics memcpy notation.
+From lrust.typing Require Export
+  lft_contexts type_context cont_context programs cont type
+  int bool own uniq_bor shr_bor uninit product sum fixpoint function
+  product_split borrow type_sum.
+
+(* Last, so that we make sure we shadow the defintion of delete for
+   collections coming from the prelude. *)
+From lrust.lang Require Export new_delete.
-- 
GitLab