aboutsummaryrefslogtreecommitdiff
path: root/theories/Reals/ClassicalDedekindReals.v
AgeCommit message (Expand)Author
2021-02-19Make most of DRealAbstr opaque.Guillaume Melquiond
2020-06-09CReal: changed epsilon for modulus of convergence from 1/n to 2^zMichael Soegtrop
2020-04-19Use binary integers for Cauchy realsVincent Semeria
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-10-24Replace classical reals quotient axioms by functional extensionality. Define ...Vincent Semeria