diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-04-12 10:08:05 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-05-15 09:58:47 +0200 |
| commit | 15059d887c3059e6d925310be860dd2a3cf97796 (patch) | |
| tree | e0c769cbad3b137e738c3e9da766f7f5f5795428 /test-suite/Makefile | |
| parent | 3008ce85ed4de549816a1cac4701cb28bee4fad6 (diff) | |
[ssr] import ssreflect test suite from math-comp
Diffstat (limited to 'test-suite/Makefile')
| -rw-r--r-- | test-suite/Makefile | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 9d84cd5c7..2531b8c67 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -94,7 +94,7 @@ INTERACTIVE := interactive VSUBSYSTEMS := prerequisite success failure $(BUGS) output \ output-modulo-time $(INTERACTIVE) micromega $(COMPLEXITY) modules stm \ - coqdoc + coqdoc ssr # All subsystems SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile @@ -158,6 +158,7 @@ summary: $(call summary_dir, "Complexity tests", complexity); \ $(call summary_dir, "Module tests", modules); \ $(call summary_dir, "STM tests", stm); \ + $(call summary_dir, "SSR tests", ssr); \ $(call summary_dir, "IDE tests", ide); \ $(call summary_dir, "VI tests", vio); \ $(call summary_dir, "Coqchk tests", coqchk); \ @@ -261,7 +262,8 @@ $(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v fi; \ } > "$@" -$(addsuffix .log,$(wildcard success/*.v micromega/*.v modules/*.v)): %.v.log: %.v $(PREREQUISITELOG) +ssr: $(wildcard ssr/*.v:%.v=%.v.log) +$(addsuffix .log,$(wildcard ssr/*.v success/*.v micromega/*.v modules/*.v)): %.v.log: %.v $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ opts="$(if $(findstring modules/,$<),-R modules Mods -impredicative-set)"; \ |