1 files changed, 1 insertions, 3 deletions

diff --git a/Makefile b/Makefile
index 86587714..5fdd3737 100644
--- a/Makefile
+++ b/Makefile
@@ -198,10 +198,8 @@ tfstarp-%: BACKEND_SUBDIR := fstar
 tfstarp-%:
 	$(AENEAS_CMD)
 
-# TODO: -test-trans-units
-# It doesn't work on vec_push_fwd, I don't understand why.
 .PHONY: tcoq-%
-tcoq-%: OPTIONS += -backend coq
+tcoq-%: OPTIONS += -backend coq -test-trans-units
 tcoq-%: BACKEND_SUBDIR := coq
 tcoq-%:
 	$(AENEAS_CMD)