k32 (Nov 14 2020 at 22:16): k32 (Nov 14 2020 at 22:16):Hello everyone. Is there some way to make a hyperlink to another module in coqdoc? [Module] doesn't do the job, it seems like it only works with definitions. P.S. I got around to writing some coqdocs for the first time, so probably more questions will pop up.
Li-yao (Nov 15 2020 at 17:02):There is an --interpolate option that enables hyperlinking in coqdoc comments, but it's pretty hacky because it only recognizes names that appear elsewhere in the module (in the actual code rather than the comments).
Last updated: Oct 13 2024 at 01:02 UTC