coq - The formal proof system

Age	Commit message (Expand)	Author
2019-11-01	docs: Add refman+stdlib documentation	Erik Martin-Dorel
2019-11-01	Add "==", "<", "<=" in PrimFloat.v	Erik Martin-Dorel
2019-11-01	Make primitive float work on Windows	Pierre Roux
2019-11-01	Reimplement is_float	Pierre Roux
2019-11-01	Make primitive float work on x86_32	Pierre Roux
2019-11-01	Pretty-printing primitive float constants	Erik Martin-Dorel
2019-11-01	Parsing primitive float constants	Pierre Roux
2019-11-01	Add primitive floats to checker	Pierre Roux
2019-11-01	Add tests for primitive floats with 'native_compute'	Pierre Roux
2019-11-01	Add primitive floats to 'native_compute'	Pierre Roux
2019-11-01	Add next_{up,down} primitive float functions	Pierre Roux
2019-11-01	Implement classify on primitive float	Pierre Roux
2019-11-01	Change return type of primitive float comparison	Pierre Roux
2019-11-01	Put axioms on ldshiftexp and frshiftexp	Guillaume Bertholon
2019-11-01	Add tests for primitive floats with 'vm_compute'	Guillaume Bertholon
2019-11-01	Add primitive floats to 'vm_compute'	Guillaume Bertholon
2019-11-01	Add tests for primitive floats	Guillaume Bertholon
2019-11-01	Add Floats to standard library	Guillaume Bertholon
2019-11-01	Add primitive floats to Ltac2	Pierre Roux
2019-11-01	Add primitive float computation in Coq kernel	Guillaume Bertholon
2019-11-01	Declare type of primitives in CPrimitives	Pierre Roux
2019-10-31	Merge PR #11021: Fix build in master	Pierre-Marie Pédrot
2019-10-31	lra: use “lia” rather than “omega”	Vincent Laporte
2019-10-31	Merge PR #10983: QArith, Lia: depend on ZArith_base rather than on ZArith	Pierre-Marie Pédrot
2019-10-31	Merge PR #10985: Print argument info as an Arguments command in About	Emilio Jesus Gallego Arias
2019-10-31	[prettyp] remove `mod_ops` and `indirect_accessor` parameters	Gaëtan Gilbert
2019-10-31	Merge PR #10994: Numbers.Cyclic: use “lia” rather than “omega”	Pierre-Marie Pédrot
2019-10-31	Merge PR #10937: [stdlib]Reals: use “lia” rather than “omega”	Pierre-Marie Pédrot
2019-10-31	Merge PR #11000: make: guard cp calls with rm -f on executables	Pierre-Marie Pédrot
2019-10-31	Merge PR #9883: Add support for Sorts in numeral notations	Vincent Laporte
2019-10-31	Merge PR #10997: Implement the unsupported attribute error using the warning ...	Emilio Jesus Gallego Arias
2019-10-31	lia: depend only on ZArith_base	Vincent Laporte
2019-10-31	QArith: only depend on ZArith_base	Vincent Laporte
2019-10-31	Zdigits: use “lia” rather than “omega”	Vincent Laporte
2019-10-31	Zquot: use “lia” rather than “omega”	Vincent Laporte
2019-10-31	Zpow_facts: use “lia” rather than “omega”	Vincent Laporte
2019-10-31	Zwf: use “lia” rather than “omega”	Vincent Laporte
2019-10-31	Zgcd_alt: use “lia” rather than “omega”	Vincent Laporte
2019-10-31	restore red behaviour printing	Gaëtan Gilbert
2019-10-31	changelog for #10985	Gaëtan Gilbert
2019-10-31	Fix output tests	Gaëtan Gilbert
2019-10-31	ppvernac: bidi hints use & not \|	Gaëtan Gilbert
2019-10-31	Print argument info as an Arguments command in About	Gaëtan Gilbert
2019-10-31	Move prettyp (Print implementation) to vernac/	Gaëtan Gilbert
2019-10-31	Doc: index command Arguments with assert	Gaëtan Gilbert
2019-10-31	Move Arguments implementation to its own file (from vernacentries)	Gaëtan Gilbert
2019-10-31	Merge PR #10861: Fix #10615: Notation substitution for Ltac2 terms.	Gaëtan Gilbert
2019-10-31	Merge PR #11009: Rename the 2 local type_cstr nonterminals to give them uniqu...	Pierre-Marie Pédrot
2019-10-31	Merge PR #10995: add test for #4502 (fixed by unknown commit)	Pierre-Marie Pédrot
2019-10-31	Merge PR #10933: Add clarification in make-changelog.	Gaëtan Gilbert