From 2d31a42aa3c2dacabc0cf005b45fc7bb4e6383e9 Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Tue, 30 Apr 2019 14:48:37 +0200
Subject: Reimplement the hierarchy related tools in OCaml

The functionalities of the structure hierarchy related tools `hierarchy-diagram`
and `hierarchy_test.py` are provided by an OCaml script `hierarchy.ml`.
`test_suite/hierarchy_test.v` is deleted. Now make can generate it.
---
 mathcomp/Makefile.coq.local | 4 ++++
 1 file changed, 4 insertions(+)
 create mode 100644 mathcomp/Makefile.coq.local

(limited to 'mathcomp/Makefile.coq.local')

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
-- 
cgit v1.2.3