aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/Makefile.coq.local
diff options
context:
space:
mode:
Diffstat (limited to 'mathcomp/Makefile.coq.local')
-rw-r--r--mathcomp/Makefile.coq.local4
1 files changed, 4 insertions, 0 deletions
diff --git a/mathcomp/Makefile.coq.local b/mathcomp/Makefile.coq.local
new file mode 100644
index 0000000..11d3121
--- /dev/null
+++ b/mathcomp/Makefile.coq.local
@@ -0,0 +1,4 @@
+test_suite/hierarchy_test.v: all/all.vo
+ mkdir -p test_suite/
+ COQBIN=$(COQBIN) ocaml ../etc/utils/hierarchy.ml -verify \
+ -R . mathcomp -lib all.all > test_suite/hierarchy_test.v