coq - The formal proof system

Age	Commit message (Expand)	Author
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
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