The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

I often want my coqdoc-generated HTML to link to specific parts of webpages.

The urls of such links contain #, e.g. :

https://hackage.haskell.org/package/base-4.8.1.0/docs/Control-Concurrent.html#v:threadDelay

Unfortunately, coqdoc uses # to mark the start and end of escaped HTML.

Here is an example of a coqdoc-comment I wanted  to write in one of my .v files:

(**

The implementation is based on the 

#<a href=""https://hackage.haskell.org/package/base-4.8.1.0/docs/Control-Concurrent.html#v:threadDelay">threadDelay</a>#

function of Haskell, whose resolution is 1 microseconds.

*)

The result is not what I want because the #  in the middle prematurely terminates

the escaped HTML.

Thanks,

-- Abhishek

http://www.cs.cornell.edu/~aa755/