aboutsummaryrefslogtreecommitdiff
path: root/theories/Reals/Abstract/ConstructiveMinMax.v
AgeCommit message (Collapse)Author
2020-05-16Prove that classical reals implement constructive reals. Also move sums, min ↵Vincent Semeria
and max to CoRN. Update stdlib index Remove ConstructiveSum from the index Add changelog entry Make constructive reals experimental