fstartactlib: Include Steel.Effect.Common automatically

FStarLang · Sep 30, 2020 · 83b8bb3 · 83b8bb3
1 parent 021bdeb
commit 83b8bb3
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 2 deletions.
diff --git a/ulib/Makefile b/ulib/Makefile
@@ -39,7 +39,7 @@ fstartaclib.mgen: fstarlib.mgen
 	rm -f .depend.extract
 	+OUTPUT_DIRECTORY=tactics_ml/extracted \
 	    CODEGEN=Plugin \
-	    EXTRACT_MODULES="--extract '+FStar.Tactics +FStar.Reflection $(NOEXTRACT_MODULES)'" \
+	    EXTRACT_MODULES="--extract '+FStar.Tactics +FStar.Reflection $(NOEXTRACT_MODULES) +Steel.Effect.Common'" \
 	    $(MAKE) -f Makefile.extract all-ml
 	mkdir -p tactics_ml/fstarlib_leftovers
 	cp $(FSTARLIB_LEFTOVERS) tactics_ml/fstarlib_leftovers

diff --git a/ulib/Makefile.extract b/ulib/Makefile.extract
@@ -11,7 +11,8 @@ FSTAR_FILES:=$(filter-out $(NOEXTRACT_FILES), \
 	$(wildcard FStar.*.fst FStar.*.fsti) \
 	$(wildcard LowStar.*.fst LowStar.*.fsti) \
 	$(wildcard legacy/*fst legacy/*fsti) \
-	$(wildcard experimental/*fst experimental/*fsti))
+	$(wildcard experimental/*fst experimental/*fsti)) \
+	Steel.Effect.Common.fst
 
 CODEGEN ?= OCaml
 MY_FSTAR=$(FSTAR) $(OTHERFLAGS) --lax --cache_checked_modules --odir $(OUTPUT_DIRECTORY) --cache_dir .cache.lax