Skip to Content.
Sympa Menu

ssreflect - [ssreflect] Online Documentation for ssrbool and ssrfun?

Subject: Ssreflect Users Discussion List

List archive

[ssreflect] Online Documentation for ssrbool and ssrfun?


Chronological Thread 
  • From: Christian Doczkal <>
  • To: "" <>
  • Subject: [ssreflect] Online Documentation for ssrbool and ssrfun?
  • Date: Tue, 4 Sep 2018 18:21:34 +0200
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None ; spf=Neutral ; spf=None
  • Ironport-phdr: 9a23:ftZrJRffQFmd0p4Isi5Q/qALlGMj4u6mDksu8pMizoh2WeGdxcW7ZB7h7PlgxGXEQZ/co6odzbaO7Oa4ASQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTahY75+Ngm6oRnMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+t6LplSALziCcfKTE27H3XhMJ3jKJeuh2hphp/yJPQbIyaMPdye6XQds4YS2VcRMZcTzJPDIOhYYUMAeQOM+lXoJXyqVYVsRuzBxOhCP/zxjJGhHL727Ax3eQ7EQHB2QwtB8wDsHTOrNX0L6cSTeG1w7POzT7eYf1W3ivy6YnLch87pfGHQLV9ftbRyUk1FgPFlUmQqY3/MDOTzOgCrm+b4PZhVOKskWEnrxp8rSapxsc3k4XJgoIUylfC9SljzoY1P8S1RUhmatCqF5tQsjuVN4pwQs46QmFovjw6yrwctpKhcigK0owrxxHea/ybc4iI/wnsWPyQITd/gn9uZbGxhw6q/ES9xeDwStO43VRIoyZfj9XBt3IA2wbN5sSZVPdx5lqt1DmT2wzJ6OxJI1o4mbfVJpI7xrM9mJweulnZECDsgkX5lqqWe10k+ue27+TnZa3rppuGOIBvkQ7xLL4ildK5AeQjKwQOW2ia+eO61LH58035Wq1GjvwwkqbHrJDXPdkXq6GlDwNP0Isu6QyzAyqn3dkah3ULMkxJdAyfg4jsIV7OIfT4Dfmlg1SrlTdm3+zJPr37ApXMNXjDjLbhcqx760JG1QUzysxQ5pNXCr4bJPL+QVH+tNrDDhMgNwy1w+HnCNNn2oMQQ2KDGrWZP7/KsV+U+uIvJPGBZJQOuDbnNfcl6frugmElll8BZqSpxpsWaHWgHvt8OUmZYHzsgs0AEWgQpAY+Qvbq2xW+VmsZfG2oUqw46zonIIe9F8LCQJqsifqA2j26F9tYfCoOXkuXC3rmc4iPR98JczjXI8l7kzVCVL67SoZn2wv45yHgzL8yBerO+zYEtJvlnPRy7P/QnBV6oTd0FcWGz2CESSd4mWgaRDYy9K15ugl521CFl6Zi1a8LXedP7u9EB19pfaXXyPZ3XoyjA1OTTpKyUF+jB+6eL3Q0R9M1zcUJZh8mSdiklVXHzi2sRbEPxebSWM4Et5nE1n20HP5Tjm7c3fB63VQgWY5LJGqgwKBlpVCKWtz51n6BnqPvTpwymS7A8GDanDiKtUtSXUh9V76AWWEYYA3Yt4ah6w==
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

Archive powered by MHonArc 2.6.18.

Top of Page