Merge pull request #83 from AeneasVerif/son/backs

Remove the option to split the forward/backward functions

1 files changed, 0 insertions, 49 deletions

diff --git a/tests/fstar-split/demo/Makefile b/tests/fstar-split/demo/Makefile
deleted file mode 100644
index fa7d1f36..00000000
--- a/tests/fstar-split/demo/Makefile
+++ /dev/null
@@ -1,49 +0,0 @@
-# This file was automatically generated - modify ../Makefile.template instead
-INCLUDE_DIRS = .
-
-FSTAR_INCLUDES = $(addprefix --include ,$(INCLUDE_DIRS))
-
-FSTAR_HINTS ?= --use_hints --use_hint_hashes --record_hints
-
-FSTAR_OPTIONS = $(FSTAR_HINTS) \
-  --cache_checked_modules $(FSTAR_INCLUDES) --cmi \
-  --warn_error '+241@247+285-274' \
-
-FSTAR_EXE ?= fstar.exe
-FSTAR_NO_FLAGS = $(FSTAR_EXE) --already_cached 'Prims FStar LowStar Steel' --odir obj --cache_dir obj
-
-FSTAR = $(FSTAR_NO_FLAGS) $(FSTAR_OPTIONS)
-
-# The F* roots are used to compute the dependency graph, and generate the .depend file
-FSTAR_ROOTS ?= $(wildcard *.fst *.fsti)
-
-# Build all the files
-all: $(addprefix obj/,$(addsuffix .checked,$(FSTAR_ROOTS)))
-
-# This is the right way to ensure the .depend file always gets re-built.
-ifeq (,$(filter %-in,$(MAKECMDGOALS)))
-ifndef NODEPEND
-ifndef MAKE_RESTARTS
-.depend: .FORCE
-	$(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) > $@
-
-.PHONY: .FORCE
-.FORCE:
-endif
-endif
-
-include .depend
-endif
-
-# For the interactive mode
-%.fst-in %.fsti-in:
-	@echo $(FSTAR_OPTIONS)
-
-# Generete the .checked files in batch mode
-%.checked:
-	$(FSTAR) $(FSTAR_OPTIONS) $< && \
-	touch -c $@
-
-.PHONY: clean
-clean:
-	rm -f obj/*