diff --git a/_CoqProject b/_CoqProject
index cccad2edc01b9bb49dde765090e8a2b7537e5f21..5cabedc486f98ba582a375296f19b288b1ffad0a 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -34,3 +34,5 @@ theories/typing/uniq_bor.v
 theories/typing/shr_bor.v
 theories/typing/own.v
 theories/typing/borrow.v
+theories/typing/product_split.v
+theories/typing/type_sum.v