1 files changed, 1 insertions, 0 deletions
diff --git a/Makefile b/Makefile
index 70e20ac72e..fe8d729084 100644
--- a/Makefile
+++ b/Makefile
@@ -301,6 +301,7 @@ SUBTACCMO=\
 	contrib/subtac/context.cmo \
 	contrib/subtac/subtac_errors.cmo \
 	contrib/subtac/subtac_coercion.cmo \
+	contrib/subtac/subtac_pretyping_F.cmo \
 	contrib/subtac/subtac_pretyping.cmo \
 	contrib/subtac/subtac_interp_fixpoint.cmo \
 	contrib/subtac/subtac_command.cmo \