coq-mathcomp-reals package - #1349

Merged

affeldt-aist merged 10 commits into

math-comp:masterfrom

proux01:reals_package

Oct 28, 2024

Commits on Oct 28, 2024

Remove a few useless constraints in opam file
proux01
committed
ccca478
Reduce dependencies of showcase/summability.v
proux01
committed
ab8a38d
Reduce dependencies of nsatz_realtype.v
proux01
committed
1764db6
Remove dependency from real_interval.v on normedtype.v
proux01
committed
2e80467
Split Rstruct.v into Rstruct.v and Rstruct_topology.v
proux01
committed
769fc2f
Add a coq-mathcomp-reals package
proux01
committed
ae26a8e
Add Opam packages
proux01
committed
1899c41
Adapt packager script from mathcomp
proux01
committed
797bfd4
[CI] Test Nix overlay
proux01
committed
7ed7166
Add changelog
proux01
committed
76e5d2d