replace posnum.v
by signed.v
from the forthcoming coq-mathcomp-reals
package?
#29
Labels
enhancement
New feature or request
apery/theories/posnum.v
Line 1 in da803b7
I noticed that this repository contains a copy of
posnum.v
from a past version of MathComp-Analysis.It has since been reimplemented (and improved) as
signed.v
and it will soon be made available as a lightweightpackage (
coq-mathcomp-reals
? see https://github.com/math-comp/analysis/tree/master/reals) so that you can use it without needing MathComp-Analysis. @proux01That would also contribute to solve issue #10 .
The text was updated successfully, but these errors were encountered: