diff --git a/testcases/regression/Holmakefile b/testcases/regression/Holmakefile index 6c6bfcf5c0c61370fdc2a923ffc1881614d1fddf..edc96554271b756e412d6f00acc0e1b1026e9cbd 100644 --- a/testcases/regression/Holmakefile +++ b/testcases/regression/Holmakefile @@ -1,27 +1,7 @@ INCLUDES = $(HOLDIR)/examples/machine-code/hoare-triple ../../hol4 ../../hol4/Infra OPTIONS = QUIT_ON_FAILURE -ifdef POLY -HOLHEAP = heap -EXTRA_CLEANS = $(HOLHEAP) $(HOLHEAP).o -all: $(HOLHEAP) - THYFILES = $(patsubst %Script.sml,%Theory.uo,$(wildcard *.sml)) TARGETS = $(patsubst %.sml,%.uo,$(THYFILES)) -all: $(TARGETS) $(HOLHEAP) +all: $(TARGETS) .PHONY: all - -BARE_THYS = BasicProvers Defn HolKernel Parse Tactic monadsyntax \ - alistTheory arithmeticTheory bagTheory boolLib boolSimps bossLib \ - combinTheory dep_rewrite finite_mapTheory indexedListsTheory lcsymtacs \ - listTheory llistTheory markerLib realTheory realLib RealArith\ - optionTheory pairLib pairTheory pred_setTheory \ - quantHeuristicsLib relationTheory res_quanTheory rich_listTheory \ - sortingTheory sptreeTheory stringTheory sumTheory wordsTheory \ - simpLib realTheory realLib RealArith - -DEPS = $(patsubst %,%.uo,$(BARE_THYS1)) $(PARENTHEAP) - -$(HOLHEAP): $(DEPS) - $(protect $(HOLDIR)/bin/buildheap) -o $(HOLHEAP) $(BARE_THYS) -endif