aboutsummaryrefslogtreecommitdiff
path: root/theories/Reals/Abstract/ConstructiveSum.v
AgeCommit message (Expand)Author
2020-05-09Define CRzero and CRone via CR_of_QVincent Semeria
2020-03-27Cleanup stdlib reals. Use implicit arguments for ConstructiveReals. Move Cons...Vincent Semeria
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-05 09:40:00 +0000