coq - The formal proof system

Age	Commit message (Expand)	Author
2019-11-01	Add a check for gradual underflows	Pierre Roux
2019-11-01	Add the IEEE-754 arch requirement in INSTALL	Pierre Roux
2019-11-01	feat: Use SSE2_MATH if available & Die if missing on x87	Erik Martin-Dorel
2019-11-01	Fix ldshiftexp	Pierre Roux
2019-11-01	Add overlays	Pierre Roux
2019-11-01	docs: Add entry in changelog	Erik Martin-Dorel
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-11-01	[ssr] Update doc for under w.r.t. setoid-like relations	Erik Martin-Dorel
2019-11-01	[ssr] chore: Remove ssrclasses.{ml,mli} (now unneeded)	Erik Martin-Dorel
2019-11-01	[ssr] Refactor/Extend of under to support more relations	Erik Martin-Dorel
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	[ssr] Refactor/Simplify the implementation of under	Erik Martin-Dorel
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	enforcing Ltac2 constructor name are uppercased	Kenji Maillard
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