coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Make some comments more precise about compilation of cofixpoints	Maxime Dénès	2018-05-28
*	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-04-30
*	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	2018-03-26
*	Handle application of a primitive projection to a not yet evaluated cofixpoin...	Guillaume Melquiond	2016-12-23
*	Fix #5248 - test-suite fails in 8.6beta1	Maxime Dénès	2016-12-06
*	Fix incorrect long multiplication in the VM.	Guillaume Melquiond	2016-11-24
*	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-10-26
\|\
\| *	Fix #5127 Memory corruption with the VM	Maxime Dénès	2016-10-24
* \|	More comments in VM.	Maxime Dénès	2016-10-19
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-06-01
\|\\|
\| *	Fix potential race condition in vm_compute.	Guillaume Melquiond	2016-05-31
* \|	Remove int64 emulation in bytecode interpreter.	Maxime Dénès	2016-03-25
\|/
*	Adds support for the virtual machine to perform reduction of universe polymor...	Gregory Malecha	2015-10-28
*	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-14
*	Code cleaning in VM (with Benjamin).	Maxime Dénès	2015-10-09
*	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-09-06
*	Fix handling of primitive projections in VM.	Maxime Dénès	2015-07-05
*	Making Coq compile with ocp-memprof.	Pierre-Marie Pédrot	2015-06-01
*	Fix some ill-typed debugging code in the VM.	Guillaume Melquiond	2015-04-27
*	fix code and bound for SWITCH instruction.	Benjamin Gregoire	2015-03-30
*	allows the vm to deal with inductive type with 8388607 constant constructors ...	Benjamin Gregoire	2015-03-26
*	Fix compilation with forthcoming Ocaml version 4.03.	Arnaud Spiwack	2015-03-13
*	Switch the few remaining iso-latin-1 files to utf8	Pierre Letouzey	2014-12-09
*	Remove some dead code in the vm	letouzey	2012-10-02
*	fast bitwise operations (lor,land,lxor) on int31 and BigN	letouzey	2012-08-11
*	Fix thumb2-related build error	glondu	2011-04-19
*	CHANGES: a word about recent changes in coqide, about Ctrl-C in vm	letouzey	2011-04-01
*	Checks for signals in VM, allowing it to be interrupted by Ctrl-C (experimental)	letouzey	2011-04-01
*	Some dead code removal, thanks to Oug analyzer	letouzey	2010-09-24
*	Discontinue support for ocaml 3.09.*	letouzey	2010-05-19
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	ocamlbuild improvements + minor makefile fix	letouzey	2009-03-24
*	Many changes in the Makefile infrastructure + a beginning of ocamlbuild	letouzey	2009-03-20
*	Rely on ocamlc to call the C compiler...	glondu	2008-09-04
*	Correction du problème de complexité de Print Assumptions :	aspiwack	2008-05-27
*	Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaient	herbelin	2008-04-01
*	patch for C code of addmuldiv31	thery	2008-02-27
*	* Adding compability with ocaml 3.10 + camlp5 (rework of	letouzey	2007-09-15
*	ajout de head0 et tail0 en natif	bgregoir	2007-06-20
*	corrections bug dans l'implem de int31	bgregoir	2007-05-15
*	Processor integers + Print assumption (see coqdev mailing list for the	aspiwack	2007-05-11
*	Changement dans le kernel :	bgregoir	2006-12-11
*	changement des _sym par _comm dans setoid_ring	bgregoir	2006-10-27
*	Appel à caml_modify pour Ocaml 3.07	notin	2006-09-01