Stream: Coq users

Topic: Coqdoc markup

view this post on Zulip 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.

view this post on Zulip 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: Jun 16 2024 at 03:41 UTC