From 6eab7f1d8eeb7826d44c6bbacf24935965c8f7da Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 14 Nov 2022 09:33:19 +0100
Subject: Reactivate the option -test-trans-unis for Coq

---
 Makefile | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'Makefile')

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)
-- 
cgit v1.2.3