coq - The formal proof system

Age	Commit message (Expand)	Author
2020-09-22	Use the closure tag for accumulators.	Guillaume Melquiond
2020-09-22	Use the same memory layout as closures for accumulators.	Guillaume Melquiond
2020-09-22	Modify bytecode representation of closures to please OCaml's GC (fix #12636).	Guillaume Melquiond
2020-07-22	Remove redundant data from VM case switch.	Pierre-Marie Pédrot
2020-07-06	Primitive persistent arrays	Maxime Dénès
2020-03-27	Merge PR #11102: Use the Alloc_small macro from the OCaml runtime rather than...	Maxime Dénès
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
2020-03-09	Do not rely on the implicit declaration of caml_minor_collection.	Guillaume Melquiond
2019-12-22	Use the Alloc_small macro from the OCaml runtime rather than our own.	Guillaume Melquiond
2019-12-17	failwith -> caml_failwith	Guillaume Munch-Maccagnoni
2019-12-17	Fatal error in VM if SIGINT was seen but no exception occured.	Guillaume Munch-Maccagnoni
2019-12-17	Fix signal polling for OCaml 4.10	Guillaume Munch-Maccagnoni
2019-12-17	[VM] fix volatile declaration	Guillaume Munch-Maccagnoni
2019-12-12	[vm] Untabify the VM C code.	Emilio Jesus Gallego Arias
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