coq - The formal proof system

Age	Commit message (Expand)	Author
2021-02-19	Remove some trivial definition.	Guillaume Melquiond
2021-02-19	Abstract the non-computational part away.	Guillaume Melquiond
2021-02-19	Terminate some lemmas with Qed.	Guillaume Melquiond
2020-06-09	CReal: changed epsilon for modulus of convergence from 1/n to 2^z	Michael Soegtrop
2020-05-16	Prove that classical reals implement constructive reals. Also move sums, min ...	Vincent Semeria
2020-05-09	Define CRzero and CRone via CR_of_Q	Vincent Semeria
2020-05-03	Simplify division of Cauchy reals	Vincent Semeria
2020-04-30	Replace QSeqEquiv by QCauchySeq, simplify proofs.	Vincent Semeria
2020-04-29	Reduce rational numbers in Cauchy real addition, to accelerate it	Vincent Semeria
2020-04-22	Document Cauchy reals	Vincent Semeria
2020-04-19	Use binary integers for Cauchy reals	Vincent Semeria
2020-04-18	Make multiplication of Cauchy reals transparent and accelerate it	Vincent Semeria
2020-03-27	Cleanup stdlib reals. Use implicit arguments for ConstructiveReals. Move Cons...	Vincent Semeria