coq - The formal proof system

Age	Commit message (Expand)	Author
2020-03-27	Cleanup stdlib reals. Use implicit arguments for ConstructiveReals. Move Cons...	Vincent Semeria
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
2019-10-24	Replace classical reals quotient axioms by functional extensionality. Define ...	Vincent Semeria
2019-09-16	Define morphisms of real numbers and accelerate Cauchy reals	Vincent Semeria
2019-08-19	Split ConstructiveRealsLUB and improve comments	Vincent Semeria
2019-08-09	Switch constructive Rlt to sort Type, to make it compute later	Vincent Semeria
2019-08-08	Fix namespace of Cauchy reals	Vincent Semeria
2019-08-08	Add interface of constructive real numbers, with an opaque implementation by ...	Vincent Semeria
2019-08-06	Prove the completeness of real numbers from logical axiom sig_not_dec	Vincent Semeria
2019-07-17	Rename ConstructiveRIneq and ConstructiveRcomplete	Vincent Semeria