diff --git a/.github/workflows/generate_docs.yml b/.github/workflows/generate_docs.yml
index e76a4fdf7..a14e3aedd 100644
--- a/.github/workflows/generate_docs.yml
+++ b/.github/workflows/generate_docs.yml
@@ -38,7 +38,7 @@ jobs:
         run: opam install -y --deps-only . && opam exec -- make -j 4
 
       - name: Install Rocqnavi
-        run: opam install -y rocq-navi
+        run: opam install -y rocq-navi.0.3.1
 
       - name: Generate Documents
         run: |
diff --git a/Makefile.common b/Makefile.common
index 6422f2d73..a41d819c9 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -132,33 +132,16 @@ $(DOCDIR)/dependency_graph.dot: $(DOCDIR)/dependency_graph.pre
 	tred $(DOCDIR)/dependency_graph.pre > $(DOCDIR)/dependency_graph.dot
 
 html: build $(DOCDIR)/dependency_graph.dot
+	etc/rocqnavi_generate-hierarchy-graph.sh $(DOCDIR)/hierarchy_graph.dot
 	mkdir -p $(DOCDIR)
 	find . -not -path '*/.*' -name "*.v" -or -name "*.glob" | xargs rocqnavi \
 	-title "Mathcomp Analysis" \
 	-d $(DOCDIR) -base mathcomp -Q theories analysis \
 	-coqlib https://rocq-prover.org/doc/V8.20.1/stdlib/ \
 	-dependency-graph $(DOCDIR)/dependency_graph.dot \
+	-hierarchy-graph $(DOCDIR)/hierarchy_graph.dot \
+        -index-blacklist etc/rocqnavi_index-blacklist \
+        -show-type-information-using-coqtop-process \
 	-external https://math-comp.github.io/htmldoc_2_3_0/ mathcomp.ssreflect \
 	-external https://math-comp.github.io/htmldoc_2_3_0/ mathcomp.algebra
 
-machtml: build $(DOCDIR)/dependency_graph.dot
-	coqdep -f _CoqProject > depend.d
-	cat -n depend.d >&2
-	gsed -i 's/Classical/mathcomp\.classical/' depend.dot
-	gsed -i 's/Theories/mathcomp\.analysis/' depend.dot
-	gsed -i 's/Reals_stdlib/mathcomp\.reals_stdlib/' depend.dot
-	gsed -i 's/Experimental_reals/mathcomp\.experimental_reals/' depend.dot
-	gsed -i 's/Reals/mathcomp\.reals/' depend.dot
-	gsed -i 's/Analysis_stdlib/mathcomp\.analysis_stdlib/' depend.dot
-	gsed -i 's/\//\./g' depend.dot
-	../coq2html/tools/generate-hierarchy-graph.sh
-	rm test_interval_inference.glob
-	find . -not -path '*/.*' -name "*.v" -or -name "*.glob" | xargs ../coq2html/rocqnavi \
-	-title "Mathcomp Analysis" \
-	-d $(DOCDIR) -base mathcomp -Q theories analysis \
-	-coqlib https://rocq-prover.org/doc/V8.20.1/stdlib/ \
-	-hierarchy-graph "hierarchy-graph.dot" \
-	-dependency-graph $(DOCDIR)/dependency_graph.dot \
-	-external https://math-comp.github.io/htmldoc_2_3_0/ mathcomp.ssreflect \
-	-external https://math-comp.github.io/htmldoc_2_3_0/ mathcomp.algebra \
-	-index-blacklist ../coq2html/tools/index-blacklist
diff --git a/etc/rocqnavi_generate-hierarchy-graph.sh b/etc/rocqnavi_generate-hierarchy-graph.sh
new file mode 100755
index 000000000..aeaa8e98d
--- /dev/null
+++ b/etc/rocqnavi_generate-hierarchy-graph.sh
@@ -0,0 +1,12 @@
+DST=$1
+coqtop -Q classical mathcomp.classical -Q reals mathcomp.reals -Q reals_stdlib mathcomp.reals_stdlib -Q experimental_reals mathcomp.experimental_reals -Q theories mathcomp.analysis -Q analysis_stdlib mathcomp.analysis_stdlib <<EOF
+From HB Require Import structures.
+Require Import mathcomp.classical.all_classical.
+Require Import mathcomp.analysis.all_analysis.
+Require Import mathcomp.reals_stdlib.Rstruct.
+Require Import mathcomp.reals.all_reals.
+Import mathcomp.analysis.lebesgue_integral_theory.simple_functions.HBSimple.
+Import mathcomp.analysis.lebesgue_integral_theory.simple_functions.HBNNSimple.
+Require Import mathcomp.analysis_stdlib.Rstruct_topology.
+HB.graph "$DST".
+EOF
diff --git a/etc/rocqnavi_index-blacklist b/etc/rocqnavi_index-blacklist
new file mode 100644
index 000000000..185e624ff
--- /dev/null
+++ b/etc/rocqnavi_index-blacklist
@@ -0,0 +1,4 @@
+*__to__*
+*__canonical__*
+*_unnamed_factory_*
+*_unnamed_mixin_*