diff --git a/theories/Trocq.v b/theories/Trocq.v
index 2fbbbc0..7bee890 100644
--- a/theories/Trocq.v
+++ b/theories/Trocq.v
@@ -15,4 +15,4 @@ From elpi Require Export elpi.
 From HoTT Require Export HoTT.
 From Trocq Require Export
   HoTT_additions Hierarchy Param_Type Param_forall Param_arrow Database Param
-  Param_paths Vernac Common.
+  Param_paths Vernac Common Param_nat Param_trans Param_bool.