From 0dc9d248080836c838cee5df28855665f81194b7 Mon Sep 17 00:00:00 2001 From: Yoshihiro Imai Date: Wed, 1 Jul 2026 13:51:02 +0900 Subject: [PATCH] Rocqnavi: :bug: Fix broken links caused by the separation of the ssreflect namespace in Math-Comp 2.5 (issue-168) --- Makefile.common | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile.common b/Makefile.common index fe936656b..21375da9c 100644 --- a/Makefile.common +++ b/Makefile.common @@ -119,5 +119,5 @@ html: build $(DOCDIR)/dependency_graph.dot -index-blacklist etc/rocqnavi_index-blacklist \ -show-type-information-using-coqtop-process \ -external https://math-comp.github.io/htmldoc_2_5_0/ mathcomp.order \ - -external https://math-comp.github.io/htmldoc_2_5_0/ mathcomp.ssreflect \ + -external https://math-comp.github.io/htmldoc_2_5_0/ mathcomp.boot \ -external https://math-comp.github.io/htmldoc_2_5_0/ mathcomp.algebra