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-10-24	Replace classical reals quotient axioms by functional extensionality. Define ↵	Vincent Semeria
	homotopy propositions and homotopy sets. Rename local variable R in test Nsatz, to avoid a name collision with the type of real numbers.
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

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
	Cauchy reals
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