Skip to Content.
Sympa Menu

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

Subject: Ssreflect Users Discussion List

List archive

Re: [ssreflect] Online Documentation for ssrbool and ssrfun?


Chronological Thread 
  • From: Enrico Tassi <>
  • To:
  • Subject: Re: [ssreflect] Online Documentation for ssrbool and ssrfun?
  • Date: Tue, 4 Sep 2018 22:17:39 +0200
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None ; spf=None ; spf=None
  • Ironport-phdr: 9a23:RBSgKhcorgp4NHSfMqolHsUKlGMj4u6mDksu8pMizoh2WeGdxcS4Yh7h7PlgxGXEQZ/co6odzbaO7Oa4ASQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTahY75+Ngm6oRnMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+t6LplSALziCcfKTE27H3XhMJ3jKJeuh2hphp/yJPQbIyaMPdye6XQds4YS2VcRMZcTyJPDIOiYYUSDOQBM+lXoJXgqFQMoxSzHhWsCP/1xzNUmnP7x7M23uI8Gg/GxgwgGNcOvWzbotXzLqcSUPy6zK7VxjvddfxWwiz96InVeR0mv/6MW6hwccvNxkkoDQ/Fkk+fqZf+PzOUzekNsm6b7/BhVe21kWInpRtxryGpy8wxhIfJgYcVxUrF9SV/2Is1JNu4SFR6YdG+CpdQuTuaO5N5QsMjX2FouDs6xaYctZ66eygG0Jsnxx/Da/yHboiH+QjvW/qWITd9gn9uZbGxhw6q/EWkxeDwTNe43VhQoidEltTArG0B2wLR58SfSfZw/V2t1SuN2g3Q8O1JJU85mbDGJ5I937I9kIcYv17ZES/sgkr2ibebdkU69eis7OTqervmqYGAN49olwH+NLguldalDeQ/KAgOUHCX+eW61LL94U30WLFHg/IsnqXHvp3WP8UWq6qjDwNIzIou6Q6zDzK839QZmXkHIkhFeBWCj4XxNFHBOur4Aumkg1m3njdk2ezGPqH8ApXLMnjMiq3tfbFn605T0AYz18xQ54pICrEdJ/L+QlTxtMfCDhAnPQy0x/joB8lh1o4FQmKOAqqZMLvIvlOS5+IvJfOMZI4PtzrnJfgl/a2msXhsgkQHcKet0JALQHWjBLFnJV+YaDzthM0AGCEEpFkQVuvv3XCESz9YYD6OVrkn53lvBYS8DIzEAJykm6eA9Ca9BJxfIG5cXAPfWUz0fpmJDq9fIBmZJdVsx2BVDOnze8oazRir8TTC5f9iJ+vQ9DcfsMu/htZ4+/HOkw07sztuAJbFij3ffyRPhmoNAgQO8uVnu0UkkgWC17J5irpWD44Lvq4bYkIBLZfZitdCJZXyVwbGJ4vbRlu6XsigHTh3Scg+kYcD
On Tue, Sep 04, 2018 at 06:21:34PM +0200, 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?

I'm trying to fix that problem. Since 8.7 these files are part of Coq.
See https://github.com/coq/coq/pull/8400

Best
--
Enrico Tassi

Archive powered by MHonArc 2.6.18.

Top of Page