From b651b0c34ff32d16ae1bca63328d42539402309a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Tue, 18 Feb 2025 16:15:51 -0800 Subject: [PATCH] Remove more --extract_module --- test/sepcomp/a/Makefile | 3 +-- test/sepcomp/b/Makefile | 3 +-- 2 files changed, 2 insertions(+), 4 deletions(-) diff --git a/test/sepcomp/a/Makefile b/test/sepcomp/a/Makefile index 84a2d119..1b496ec9 100644 --- a/test/sepcomp/a/Makefile +++ b/test/sepcomp/a/Makefile @@ -112,8 +112,7 @@ obj: .PRECIOUS: obj/%.ml obj/%.ml: - $(FSTAR) $< --codegen OCaml \ - --extract_module $(basename $(notdir $(subst .checked,,$<))) + $(FSTAR) $< --codegen OCaml # By default, krml extraction in F* will extract every module into a # single out.krml file. Make sure to extract the single module we want diff --git a/test/sepcomp/b/Makefile b/test/sepcomp/b/Makefile index 4f2e4109..1ef3b99b 100644 --- a/test/sepcomp/b/Makefile +++ b/test/sepcomp/b/Makefile @@ -114,8 +114,7 @@ obj: .PRECIOUS: obj/%.ml obj/%.ml: - $(FSTAR) $< --codegen OCaml \ - --extract_module $(basename $(notdir $(subst .checked,,$<))) + $(FSTAR) $< --codegen OCaml # By default, krml extraction in F* will extract every module into a # single out.krml file. Make sure to extract the single module we want