coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	[api] Deprecate a couple of aliases that we missed.	Emilio Jesus Gallego Arias	2018-03-28
*	Merge PR #6769: Split closure cache and remove whd_both	Maxime Dénès	2018-03-09
\|\
\| *	Pass the constant cache as a separate argument in kernel reduction.	Pierre-Marie Pédrot	2018-03-04
* \|	Update headers following #6543.	Théo Zimmermann	2018-02-27
\|/
*	[cbv] Fix evaluation of cofixpoints under primitive projections.	Maxime Dénès	2018-01-29
*	[api] Remove aliases of `Evar.t`	Emilio Jesus Gallego Arias	2017-11-26
*	Fix #5761: cbv on undefined evars under binders produces unbound rel	Gaëtan Gilbert	2017-11-15
*	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Added support for a side effect on constants in reduction functions.	Thomas Sibut-Pinote	2017-06-04
*	[option] Remove support for non-synchronous options.	Emilio Jesus Gallego Arias	2017-05-24
*	Added an option Set Debug Cbv.	Hugo Herbelin	2017-05-03
*	Removing various compatibility layers of tactics.	Pierre-Marie Pédrot	2017-02-14
*	Cbv API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)	Pierre Letouzey	2016-07-03
*	Separate flags for fix/cofix/match reduction and clean reduction function names.	Maxime Dénès	2016-07-01
*	Fix incorrect cbv reduction of primitive projections. (Bug #4634)	Guillaume Melquiond	2016-04-29
*	Update copyright headers.	Maxime Dénès	2016-01-20
*	Update headers.	Maxime Dénès	2015-01-12
*	Switch the few remaining iso-latin-1 files to utf8	Pierre Letouzey	2014-12-09
*	To stay closer to non-primitive projections, only unfold primitive	Matthieu Sozeau	2014-10-15
*	Fix bug 3662 by actually reducing primitive projections in cbv/compute.	Matthieu Sozeau	2014-09-27
*	Add a boolean to indicate the unfolding state of a primitive projection,	Matthieu Sozeau	2014-09-27
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Splitting Term into five unrelated interfaces:	ppedrot	2013-04-29
*	Modulification of name	ppedrot	2012-12-18
*	Monomorphization (pretyping)	ppedrot	2012-11-22
*	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot	2012-09-14
*	This patch removes unused "open" (automatically generated from	regisgia	2012-09-14
*	Updating headers.	herbelin	2012-08-08
*	Noise for nothing	pboutill	2012-03-02
*	avoid relying on weak invariant in cbv.ml	bgregoir	2011-11-25
*	Esubst: make types of substitutions & lifts private	puech	2011-08-08
*	Some dead code removal, thanks to Oug analyzer	letouzey	2010-09-24
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	fixed CBV strategy: it was too eager on terms like	barras	2009-04-21
*	pushed evar reduction in kernel	barras	2009-02-06
*	correction bugs dans Cbv (beta n-aire)	barras	2006-05-10
*	subst. explicites avec vecteurs	barras	2006-05-09
*	Changement des named_context	gregoire	2005-12-02
*	COMMITED BYTECODE COMPILER	barras	2004-10-20
*	premiere reorganisation de l\'unification	barras	2004-09-03
*	Nouvelle en-tête	herbelin	2004-07-16
*	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin	2003-05-19
*	simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = lis...	letouzey	2003-04-16
*	Nouveau comportement: Delta ne s'applique pas aux variables liées par un let	herbelin	2002-03-01
*	nouvel algo de conversion plus uniforme	barras	2001-11-29
*	GROS COMMIT:	barras	2001-11-05