diff options
| author | Maxime Dénès | 2019-11-01 15:53:30 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-11-01 15:53:30 +0100 |
| commit | fdabd4dbd6bfd60ad46fc8c945ed063860498e53 (patch) | |
| tree | 01edf91f8b536ad4acfbba39e114daa06b40f3f8 /test-suite/Makefile | |
| parent | d00c0b93ec4cb5ca48a9dc2ddf2cfd2038208ee2 (diff) | |
| parent | acdaab2a8c2ccb63df364bb75de8a515b2cef484 (diff) | |
Merge PR #9867: Add primitive floats (binary64 floating-point numbers)
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: maximedenes
Ack-by: proux01
Ack-by: silene
Ack-by: vbgl
Diffstat (limited to 'test-suite/Makefile')
| -rw-r--r-- | test-suite/Makefile | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index d9c89d7a8a..1744138d29 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -102,7 +102,7 @@ INTERACTIVE := interactive UNIT_TESTS := unit-tests VSUBSYSTEMS := prerequisite success failure $(BUGS) output output-coqtop \ output-modulo-time $(INTERACTIVE) micromega $(COMPLEXITY) modules stm \ - coqdoc ssr arithmetic ltac2 + coqdoc ssr primitive/uint63 primitive/float ltac2 # All subsystems SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile tools $(UNIT_TESTS) @@ -175,6 +175,7 @@ summary: $(call summary_dir, "Miscellaneous tests", misc); \ $(call summary_dir, "Complexity tests", complexity); \ $(call summary_dir, "Module tests", modules); \ + $(call summary_dir, "Primitive tests", primitive); \ $(call summary_dir, "STM tests", stm); \ $(call summary_dir, "SSR tests", ssr); \ $(call summary_dir, "IDE tests", ide); \ @@ -330,7 +331,7 @@ $(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v } > "$@" ssr: $(wildcard ssr/*.v:%.v=%.v.log) -$(addsuffix .log,$(wildcard ssr/*.v success/*.v micromega/*.v modules/*.v arithmetic/*.v ltac2/*.v)): %.v.log: %.v $(PREREQUISITELOG) +$(addsuffix .log,$(wildcard ssr/*.v success/*.v micromega/*.v modules/*.v primitive/*/*.v ltac2/*.v)): %.v.log: %.v $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ opts="$(if $(findstring modules/,$<),-R modules Mods)"; \ |