coq - The formal proof system

Age	Commit message (Expand)	Author
2019-12-04	[dune] Update to dune language version 2.0	Emilio Jesus Gallego Arias
2019-11-11	Have only one dune rule calling configure	Pierre Roux
2019-11-01	Communicate CFLAGS to dune	Pierre Roux
2019-11-01	Fix ldshiftexp	Pierre Roux
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	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 primitive floats to 'vm_compute'	Guillaume Bertholon
2019-07-29	Use the precondition of diveucl_21 to avoid massaging the dividend.	Guillaume Melquiond
2019-07-29	Use a more traditional definition for uint63_div21 (fixes #10551).	Guillaume Melquiond
2019-05-23	Fixing typos - Part 2	JPR
2019-05-15	Merge PR #9905: [vm] x86_64 registers	Maxime Dénès
2019-05-03	Remove now useless commented code	Pierre Roux
2019-05-03	[primitive integers] Make div21 implems consistent with its specification	Pierre Roux
2019-04-30	[vm] Backport from OCaml	Pierre Roux
2019-04-30	[vm] PPC64 registers	Pierre Roux
2019-04-30	[vm] ARM registers	Pierre Roux
2019-04-30	[vm] Arm 64 registers	Pierre Roux
2019-04-30	[vm] x86_64 registers	Pierre Roux
2019-04-15	[vm] Protect accu and coq_env	Pierre Roux
2019-03-01	[Kernel] Simpler generation of opcode files	Vincent Laporte
2019-02-04	[dune] Fix Dune build in Windows.	Emilio Jesus Gallego Arias
2019-02-04	Primitive integers	Maxime Dénès
2018-09-05	[build] Preliminary support for building Coq with `dune`.	Emilio Jesus Gallego Arias
2018-05-28	Make some comments more precise about compilation of cofixpoints	Maxime Dénès
2018-04-30	Adapt the VM GC hook to handle the no-naked-pointers option flag.	Pierre-Marie Pédrot
2018-04-30	Make the VM accumulator look like an OCaml block.	Pierre-Marie Pédrot
2018-04-30	Wrap VM bytecode used on the OCaml side in an OCaml block.	Pierre-Marie Pédrot
2018-03-26	Moving the VM global atom table to a ML reference.	Pierre-Marie Pédrot
2018-03-26	Moving the VM global data to a ML reference.	Pierre-Marie Pédrot
2016-12-23	Handle application of a primitive projection to a not yet evaluated cofixpoin...	Guillaume Melquiond
2016-12-06	Fix #5248 - test-suite fails in 8.6beta1	Maxime Dénès
2016-11-24	Fix incorrect long multiplication in the VM.	Guillaume Melquiond
2016-10-26	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot
2016-10-24	Fix #5127 Memory corruption with the VM	Maxime Dénès
2016-10-19	More comments in VM.	Maxime Dénès
2016-06-01	Merge branch 'v8.5'	Pierre-Marie Pédrot
2016-05-31	Fix potential race condition in vm_compute.	Guillaume Melquiond
2016-03-25	Remove int64 emulation in bytecode interpreter.	Maxime Dénès
2015-10-28	Adds support for the virtual machine to perform reduction of universe polymor...	Gregory Malecha
2015-10-14	Make interpreter of PROJ simpler by not using the stack.	Guillaume Melquiond
2015-10-14	Remove some unused variables.	Guillaume Melquiond
2015-10-14	Fix some typos.	Guillaume Melquiond
2015-10-09	Code cleaning in VM (with Benjamin).	Maxime Dénès
2015-09-06	Fix a bug in 31 bit arithmetic, leading to failing conversion tests.	Maxime Dénès