Ssreflect Users Discussion List

[Anton Trunov <>]

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