Ssreflect Users Discussion List

[Christian Doczkal <>]

Hello, 

I was specifically referring to the generated HTML. Since I am using opam, I 
have the .v files on my machine to browse them, but those files are not 
hyperlinked to the rest of the Coq standard library. Indeed, in the current 
library graph, "mem" links to:

https://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#mem

which doesn't exist. The link should be (note the V):

https://coq.inria.fr/distrib/V8.8.0/stdlib/Coq.ssr.ssrbool.html#mem

Unfortunately, the opam packages, both for Coq and for mathcomp, do not seem 
to generate and install the HTML documentation.

Best, 
Christian

On 09/04/2018 06:32 PM, Anton Trunov wrote:
> Hi Christian,
> 
> Coq’s GitHub has the files:
> 
> https://github.com/coq/coq/blob/master/plugins/ssr/ssrfun.v
> https://github.com/coq/coq/blob/master/plugins/ssr/ssrbool.v
> 
> Hope this helps.
> 
> Cheers,
> Anton
> 
>> On 4 Sep 2018, at 18:21, Christian Doczkal 
>> <>
>>  wrote:
>>
>> Hello,
>>
>> I noticed that the pages for ssrbool and ssrfun linked from the mathcomp
>> library graph
>> (http://math-comp.github.io/math-comp/htmldoc/libgraph.html) are now
>> essentially empty.
>>
>> This seems to be due to these files now being part of Coq (e.g,
>> Coq.ssr.ssrbool). Unfortunately, these files seem not to be linked from
>> the top level site of the standard library documentation
>> (https://coq.inria.fr/distrib/current/stdlib/), even though
>> https://coq.inria.fr/distrib/current/stdlib/Coq.ssr.ssrbool.html exists.
>>
>> And, as if this wasn't unfortunate enough, the aforementioned HTML page
>> does not include the descriptive comments at the top of the file, or
>> indeed any comments.
>>
>> So does someone know whether there is still some online version of these
>> files somewhere that includes the comments?
>>
>> Best,
>> Christian
>