I can't make a commit with a new file without forgetting to add it...

theories/typing/typing.v

+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.