aboutsummaryrefslogtreecommitdiff
path: root/theories/Reals/ConstructiveRealsLUB.v
AgeCommit message (Expand)Author
2020-03-27Cleanup stdlib reals. Use implicit arguments for ConstructiveReals. Move Cons...Vincent Semeria
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-09-16Define morphisms of real numbers and accelerate Cauchy realsVincent Semeria
2019-08-19Split ConstructiveRealsLUB and improve commentsVincent Semeria