coq - The formal proof system

Age	Commit message (Collapse)	Author
2021-02-19	Make most of DRealAbstr opaque.	Guillaume Melquiond
	The function returned by DRealAbstr starts by a call to the axiom sig_forall_dec, so it is not computable anyway.
2020-06-09	CReal: changed epsilon for modulus of convergence from 1/n to 2^z	Michael Soegtrop

2020-04-19	Use binary integers for Cauchy reals	Vincent Semeria

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.