From 3eba613a9ff9d5c265fbe2676f6bd324728d9ca4 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 14 Nov 2022 09:06:15 +0100
Subject: Implement a pass to decompose nested patterns in let-bindings

---
 Makefile | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index c4ec50ef..86587714 100644
--- a/Makefile
+++ b/Makefile
@@ -146,7 +146,7 @@ tfstarp-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS)
 # This generates very ugly code, but is good to test the translation.
 .PHONY: test-transp-betree_main
 test-transp-betree_main: transp-betree_main
-test-transp-betree_main: OPTIONS += -backend fstar -unfold-monads -test-trans-units
+test-transp-betree_main: OPTIONS += -backend fstar -test-trans-units
 test-transp-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS)
 test-transp-betree_main: BACKEND_SUBDIR := "fstar"
 test-transp-betree_main: SUBDIR:=betree_back_stateful
@@ -186,14 +186,14 @@ transp-%: gen-llbcp-% tfstarp-%
 	echo "# Test $* done"
 
 .PHONY: tfstar-%
-tfstar-%: OPTIONS += -backend fstar -unfold-monads -test-trans-units
+tfstar-%: OPTIONS += -backend fstar -test-trans-units
 tfstar-%: BACKEND_SUBDIR := fstar
 tfstar-%:
 	$(AENEAS_CMD)
 
 # "p" stands for "Polonius"
 .PHONY: tfstarp-%
-tfstarp-%: OPTIONS += -backend fstar -unfold-monads -test-trans-units
+tfstarp-%: OPTIONS += -backend fstar -test-trans-units
 tfstarp-%: BACKEND_SUBDIR := fstar
 tfstarp-%:
 	$(AENEAS_CMD)
@@ -201,7 +201,7 @@ tfstarp-%:
 # TODO: -test-trans-units
 # It doesn't work on vec_push_fwd, I don't understand why.
 .PHONY: tcoq-%
-tcoq-%: OPTIONS += -backend coq -decompose-monads
+tcoq-%: OPTIONS += -backend coq
 tcoq-%: BACKEND_SUBDIR := coq
 tcoq-%:
 	$(AENEAS_CMD)
-- 
cgit v1.2.3