coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-05-16	Prove that classical reals implement constructive reals. Also move sums, min ↵	Vincent Semeria
	and max to CoRN. Update stdlib index Remove ConstructiveSum from the index Add changelog entry Make constructive reals experimental
2020-05-09	Define CRzero and CRone via CR_of_Q	Vincent Semeria
	Add real numbers up to 10
2020-03-27	Cleanup stdlib reals. Use implicit arguments for ConstructiveReals. Move ↵	Vincent Semeria
	ConstructiveReals into new directory Abstract. Remove imports of implementations inside those Abstract files. Add changelog for constructive reals cleanup Move Cauchy reals into new directory Cauchy Update stdlib index Rename sum_f_R0 Use coqdoc comments Update doc/changelog/10-standard-library/11725-cleanup-reals.rst Co-Authored-By: Hugo Herbelin <herbelin@users.noreply.github.com> Update doc/changelog/10-standard-library/11725-cleanup-reals.rst Co-Authored-By: Hugo Herbelin <herbelin@users.noreply.github.com> Update doc/changelog/10-standard-library/11725-cleanup-reals.rst Co-Authored-By: Hugo Herbelin <herbelin@users.noreply.github.com> Improve notations