coq - The formal proof system

Age	Commit message (Expand)	Author
2019-11-01	Merge PR #11028: Update the deprecation doc of `Shrink Obligations`	Clément Pit-Claudel
2019-11-01	Merge PR #10647: Expose universe processing in comInductive.	Gaëtan Gilbert
2019-11-01	Merge PR #10022: [ssr] Generalize tactics under and over to any (Reflexive) r...	Enrico Tassi
2019-11-01	Update the deprecation doc of `Shrink Obligations`	Jason Gross
2019-11-01	Merge PR #9867: Add primitive floats (binary64 floating-point numbers)	Maxime Dénès
2019-11-01	minor cleanup of anonymous functions	Gaëtan Gilbert
2019-11-01	Expose universe processing in comInductive.	Jan-Oliver Kaiser
2019-11-01	Merge PR #8642: Compiled interfaces with -vos and -vok options	Pierre-Marie Pédrot
2019-11-01	Merge PR #11019: enforcing Ltac2 constructor name are uppercased	Pierre-Marie Pédrot
2019-11-01	adding test file for Uppercase Ltac2 constructors	Kenji Maillard
2019-11-01	enforcing Ltac2 cosntructors name are uppercase in open types	Kenji Maillard
2019-11-01	Add warnings regarding the experimental nature of the vos feature in the doc.	Pierre-Marie Pédrot
2019-11-01	Teach coq_dune about the empty .vos produced by coqc	Gaëtan Gilbert
2019-11-01	[test-suite] acknowledge coq_mafile installs .vos	Enrico Tassi
2019-11-01	[make] install .vos along with .vo	Enrico Tassi
2019-11-01	fix installation of vos files in coq Makefile	charguer
2019-11-01	a tentative patch to allow interactive session to load .vos files; (recall th...	charguer
2019-11-01	fix coq_makefile and doc for vos support.	charguer
2019-11-01	Changelog entry	Maxime Dénès
2019-11-01	additional details in the doc for -vos	charguer
2019-11-01	Implementing support for vos/vok files.	charguer
2019-11-01	Merge PR #11015: [Nix] Update reference to nixpkgs	Théo Zimmermann
2019-11-01	docs(gallina-extensions.rst): Say more on float literals extraction	Erik Martin-Dorel
2019-11-01	Communicate CFLAGS to dune	Pierre Roux
2019-11-01	Add some doc snippet in ExtrOCamlFloats.v	Erik Martin-Dorel
2019-11-01	Makefile.build: Fix rules of bin/votour{,.byte}	Erik Martin-Dorel
2019-11-01	Add extraction for primitive floats	Erik Martin-Dorel
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