aboutsummaryrefslogtreecommitdiff
path: root/mathcomp
diff options
context:
space:
mode:
Diffstat (limited to 'mathcomp')
-rw-r--r--mathcomp/Makefile.common9
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