aboutsummaryrefslogtreecommitdiffstats
path: root/unit-tests/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'unit-tests/Makefile')
-rw-r--r--unit-tests/Makefile18
1 files changed, 14 insertions, 4 deletions
diff --git a/unit-tests/Makefile b/unit-tests/Makefile
index 1ad9b57..0d4bdc1 100644
--- a/unit-tests/Makefile
+++ b/unit-tests/Makefile
@@ -11,9 +11,19 @@ COQC?=$(COQBIN)coqc
all: zchaff verit lfsc
-zchaff: $(ZCHAFFLOG) Tests_zchaff.vo
-verit: $(VERITLOG) Tests_verit.vo
-lfsc: Tests_lfsc.vo
+vernac: zchaffv veritv
+tactics: zchafft veritt lfsc
+
+zchaff: zchaffv zchafft
+zchaffv: $(ZCHAFFLOG) Tests_zchaff_vernac.vo
+zchafft: Tests_zchaff_tactics.vo
+
+verit: veritv veritt
+veritv: $(VERITLOG) Tests_verit_vernac.vo
+veritt: Tests_verit_tactics.vo
+
+lfsc: Tests_lfsc_tactics.vo
+
logs: $(OBJ)
@@ -30,4 +40,4 @@ logs: $(OBJ)
clean:
- rm -rf *~ $(ZCHAFFLOG) $(VERITLOG)
+ rm -rf *~ $(ZCHAFFLOG) $(VERITLOG) *.vo *.glob