diff options
| author | Enrico Tassi | 2020-09-12 13:24:47 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2020-09-12 13:24:47 +0200 |
| commit | cfa21928a5148f826e19aa5a78b83b5ed4e165b9 (patch) | |
| tree | 94074a147711bb91ba124d4d84905fab2565dc74 | |
| parent | a28ed91e0d3b2d03940c9b930ac516f0769f7e17 (diff) | |
avoid all.vo
| -rw-r--r-- | mathcomp/Makefile.common | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/mathcomp/Makefile.common b/mathcomp/Makefile.common index 9759158..df43b4f 100644 --- a/mathcomp/Makefile.common +++ b/mathcomp/Makefile.common @@ -63,7 +63,14 @@ TEST_DEP := build endif test_suite/test_hierarchy_all.v: $(TEST_DEP) - COQBIN=$(COQBIN) ocaml ../etc/utils/hierarchy.ml -verify -R . mathcomp -lib all.all > test_suite/test_hierarchy_all.v + COQBIN=$(COQBIN) ocaml ../etc/utils/hierarchy.ml -verify -R . mathcomp \ + -lib all_ssreflect \ + -lib all_algebra \ + -lib all_field \ + -lib all_character \ + -lib all_fingroup \ + -lib all_solvable \ + > test_suite/test_hierarchy_all.v Makefile.test-suite.coq: test_suite/test_hierarchy_all.v $(COQMAKEFILE) $(COQMAKEFILEOPTIONS) -f Make.test-suite -o Makefile.test-suite.coq |