summaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile4
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)