1 files changed, 3 insertions, 0 deletions
diff --git a/Makefile b/Makefile
index 0d2c5abe31..6edd5ca47d 100644
--- a/Makefile
+++ b/Makefile
@@ -299,6 +299,9 @@ SUBTACCMO=\
 	contrib/subtac/subtac_errors.cmo \
 	contrib/subtac/subtac_coercion.cmo \
 	contrib/subtac/interp.cmo \
+	contrib/subtac/interp_fixpoint.cmo \
+	contrib/subtac/subtac_command.cmo \
+	contrib/subtac/subtac.cmo \
 	contrib/subtac/sparser.cmo