The Coq mailing list

[Joey Dodds <jdodds AT princeton.edu>]

I remember this being poorly documented when I looked for it. I believe you can escape it with ##.

Joey

On Wed, Oct 14, 2015 at 4:32 PM Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

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/