[Date Prev][Date Next] [Thread Prev][Thread Next] [Date Index] [Thread Index]

Bug#883645: marked as done (Coq.Arith.PeanoNat missing from coq-theories)

Your message dated Thu, 24 Oct 2019 19:41:33 +0200
with message-id <87tv7ym46q.fsf@x80.org>
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 owner@bugs.debian.org
immediately.)


-- 
883645: https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=883645
Debian Bug Tracking System
Contact owner@bugs.debian.org 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 ---
Reply to: