coq - The formal proof system

Age	Commit message (Expand)	Author
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
2015-09-06	Fixed critical bug in 31 bit arithmetic of VM	Catalin Hritcu
2015-07-05	Fix handling of primitive projections in VM.	Maxime Dénès
2015-06-01	Making Coq compile with ocp-memprof.	Pierre-Marie Pédrot
2015-04-27	Fix some ill-typed debugging code in the VM.	Guillaume Melquiond
2015-03-30	fix code and bound for SWITCH instruction.	Benjamin Gregoire
2015-03-26	allows the vm to deal with inductive type with 8388607 constant constructors ...	Benjamin Gregoire
2015-03-13	Fix compilation with forthcoming Ocaml version 4.03.	Arnaud Spiwack
2014-12-09	Switch the few remaining iso-latin-1 files to utf8	Pierre Letouzey
2012-10-02	Remove some dead code in the vm	letouzey
2012-08-11	fast bitwise operations (lor,land,lxor) on int31 and BigN	letouzey