search

affeldt-aist / coq2html

An HTML documentation generator for Coq source files
GNU General Public License v2.0
1 stars 3 forks source link

links to mathcomp #9

Closed affeldt-aist closed 7 months ago

affeldt-aist commented 8 months ago

very minor: some links to mathcomp seem broken: https://math-comp.github.io/htmldoc/mathcomp.algebra.ssralg.html#GRing.Zmodule.Exports.zmodType (looks like it's not a coq2html bug but the fact that doc of Analysis master (still on MC1) should link to the doc of MC1 not MC master (MC2))

@proux01

yoshihiro503 commented 8 months ago

I think this issue can be solved by specifying the version explicitly in the URL to the external library.

https://yoshihiro503.github.io/coq2html/mathcomp.classical.cardinality.html#fimfun_zmodType