1 files changed, 2 insertions, 0 deletions
diff --git a/Makefile.ci b/Makefile.ci
index d549ed1b39..c589c95258 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -24,6 +24,7 @@ CI_TARGETS= \
     ci-coq_performance_tests \
     ci-coq_tools \
     ci-coqprime \
+    ci-deriving \
     ci-elpi \
     ci-engine_bench \
     ci-ext_lib \
@@ -74,6 +75,7 @@ ci-color: ci-bignums
 
 ci-coqprime: ci-bignums
 ci-coquelicot: ci-mathcomp
+ci-deriving: ci-mathcomp
 ci-math_classes: ci-bignums
 
 ci-corn: ci-math_classes