coq - The formal proof system

Age	Commit message (Collapse)	Author
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
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2019-09-16	Define morphisms of real numbers and accelerate Cauchy reals	Vincent Semeria
	Prove that morphisms preserve additions Fix stdlib index Prove that constructive real morphisms preserve multiplications by integers Prove that constructive real morphisms preserve multiplications by rationals Prove CReal_mult_pos_appart_zero Prove that constructive real morphisms preserve multiplications Prove that constructive real morphisms preserve divisions Rewrite convergence in sort Prop, to extract smaller programs Rewrite convergence on integers, to extract smaller programs Fix typos
2019-08-19	Split ConstructiveRealsLUB and improve comments	Vincent Semeria