Your message dated Thu, 24 Oct 2019 19:41:33 +0200
with message-id <[email protected]>
and subject line Invalid: the file doesn't exist in upstream.
has caused the Debian Bug report #883645,
regarding Coq.Arith.PeanoNat missing from coq-theories
to be marked as done.
This means that you claim that the problem has been dealt with.
If this is not the case it is now your responsibility to reopen the
Bug report if necessary, and/or fix the problem forthwith.
(NB: If you are a system administrator and have no idea what this
message is talking about, this may indicate a serious mail system
misconfiguration somewhere. Please contact [email protected]
immediately.)
--
883645: https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=883645
Debian Bug Tracking System
Contact [email protected] with problems
--- Begin Message ---
Package: coq-theories
Version: 8.4pl3dfsg-1
The package does not contain the following file:
/usr/lib/coq/theories/Arith/PeanoNat.vo
(see https://packages.debian.org/jessie/all/coq-theories/filelist)
I assume this file should be present since Coq.Arith.PeanoNat still appears
in the coq standard library documentation (
https://coq.inria.fr/library/Coq.Arith.PeanoNat.html) and in the source (
https://github.com/coq/coq/tree/master/theories/Arith).
--- End Message ---
--- Begin Message ---
The bug is invalid: the file doesn't exist in the upstream package:
https://github.com/coq/coq/tree/985f884b4a59a75522d5421138ab0b88f128a7ae/theories/Arith
Concretely, it was introduced in the 8.5 release.
E.
--- End Message ---
