coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #244.	Pierre-Marie Pédrot	2016-09-08
\|\
* \|	Use a better data structure for VM compilation of free vars.	Pierre-Marie Pédrot	2016-08-22
\| *	Make the user_err header an optional parameter.	Emilio Jesus Gallego Arias	2016-08-19
\| *	Remove errorlabstrm in favor of user_err	Emilio Jesus Gallego Arias	2016-08-19
\|/
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
*	A new infrastructure for warnings.	Maxime Dénès	2016-06-29
*	[feedback] Add optional ?loc parameter to loggers.	Emilio Jesus Gallego Arias	2016-06-25
*	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
*	Update copyright headers.	Maxime Dénès	2016-01-20
*	bug fixes to vm computation + test cases.	Gregory Malecha	2015-12-09
*	Refine Gregory Malecha's patch on VM and universe polymorphism.	Maxime Dénès	2015-10-28
*	Adds support for the virtual machine to perform reduction of universe polymor...	Gregory Malecha	2015-10-28
*	Fixing some English misspelling.	Hugo Herbelin	2015-07-29
*	Fix handling of primitive projections in VM.	Maxime Dénès	2015-07-05
*	Add a Set Dump Bytecode command for debugging purposes.	Maxime Dénès	2015-06-23
*	fix code and bound for SWITCH instruction.	Benjamin Gregoire	2015-03-30
*	use a more compact representation of non-constant constructors	Benjamin Gregoire	2015-03-27
*	allows the vm to deal with inductive type with 8388607 constant constructors ...	Benjamin Gregoire	2015-03-26
*	Fix bug 4157,	Benjamin Gregoire	2015-03-26
*	Fix vm compiler to refuse to compile code making use of inductives with	Matthieu Sozeau	2015-03-25
*	Fix some typos in comments.	Guillaume Melquiond	2015-02-23
*	Univs: Fix alias computation for VMs, computation of normal form of	Matthieu Sozeau	2015-01-17
*	Correct restriction of vm_compute when handling universe polymorphic	Matthieu Sozeau	2015-01-15
*	Update headers.	Maxime Dénès	2015-01-12
*	Fix #3282: VM confused by let bindings in fixpoints.	Maxime Dénès	2014-11-10
*	Add a boolean to indicate the unfolding state of a primitive projection,	Matthieu Sozeau	2014-09-27
*	"allows to", like "allowing to", is improper	Jason Gross	2014-08-25
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Changing Retrokwnoledge entry type from kind_of_term to constr. It seems it had	Pierre-Marie Pédrot	2014-03-14
*	Lazyconstr -> Opaqueproof	Enrico Tassi	2014-02-26
*	invalid_arg instead of raise (Invalid_argement ...)	letouzey	2013-03-12
*	kernel/declarations becomes a pure mli	letouzey	2013-02-26
*	Array.create is deprecated	pboutill	2012-12-19
*	Modulification of identifier	ppedrot	2012-12-14
*	More monomorphizations	ppedrot	2012-11-13
*	Monomorphized a lot of equalities over OCaml integers, thanks to	ppedrot	2012-11-08
*	Partial revert of Yann commit in order to use CLib.List when opening	ppedrot	2012-09-14
*	This patch removes unused "open" (automatically generated from	regisgia	2012-09-14
*	The new ocaml compiler (4.00) has a lot of very cool warnings,	regisgia	2012-09-14
*	Updating headers.	herbelin	2012-08-08
*	Noise for nothing	pboutill	2012-03-02
*	Modops: the strengthening functions can work without any env argument	letouzey	2011-05-17
*	Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks	letouzey	2011-04-03
*	Remove the "Boxed" syntaxes and the const_entry_boxed field	letouzey	2011-01-28
*	better fix to bug #2319: types are compiled in the env of the bodies	barras	2010-07-30
*	fixed bug #2105 (compilation of free de Bruijn) and missing lift of predicate...	barras	2010-07-29
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Removed $Id$ introduced inadvertently in r13005 (no more $Id$ since r12972)	herbelin	2010-05-09
*	Added a few informations about file lineages (for the most part in kernel)	herbelin	2010-05-09
*	Here comes the commit, announced long ago, of the new tactic engine.	aspiwack	2010-04-22