coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Separate flags for fix/cofix/match reduction and clean reduction function names.	Maxime Dénès	2016-07-01
*	A new infrastructure for warnings.	Maxime Dénès	2016-06-29
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
* \|	CLEANUP: in the Reduction module	Matej Kosik	2015-12-17
* \|	CLEANUP: in the Reduction module	Matej Kosik	2015-12-17
* \|	Unifying betazeta_applist and prod_applist into a clearer interface.	Hugo Herbelin	2015-12-05
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-29
\|\\|
\| *	Conversion of polymorphic inductive types was incomplete in VM and native.	Maxime Dénès	2015-10-28
* \|	Merge branch 'v8.5' into trunk	Maxime Dénès	2015-10-16
\|\\|
\| *	Remove left2right reference from the kernel.	Maxime Dénès	2015-10-16
\| *	Fix #4346 1/2: native casts were not inferring universe constraints.	Maxime Dénès	2015-10-15
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-15
\|\\|
\| *	Remove reference to default conversion function inside the kernel.	Maxime Dénès	2015-10-14
* \|	Splitting kernel universe code in two modules.	Pierre-Marie Pédrot	2015-10-06
\|/
*	Update headers.	Maxime Dénès	2015-01-12
*	Providing a -type-in-type option for collapsing the universe hierarchy.	Hugo Herbelin	2014-09-13
*	Use kernel conversion on terms that contain universe variables during unifica...	Matthieu Sozeau	2014-07-20
*	Make kernel reduction code parametric over the handling of universes,	Matthieu Sozeau	2014-06-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	Support for evars and metas in native compiler.	Maxime Dénès	2013-12-30
*	Tentative fix of the guardedness checker by Christine and me. All stdlib and ...	Matthieu Sozeau	2013-12-17
*	Splitting Term into five unrelated interfaces:	ppedrot	2013-04-29
*	New implementation of the conversion test, using normalization by evaluation to	mdenes	2013-01-22
*	Updating headers.	herbelin	2012-08-08
*	Propagated information from the reduction tactics to the kernel so	herbelin	2011-08-10
*	- Remove create_evar_defs	msozeau	2011-04-13
*	Starting being more explicit on the reasons why module subtyping fails.	herbelin	2011-03-05
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	New script dev/tools/change-header to automatically update Coq files headers.	herbelin	2010-06-22
*	"Improved" the form of the inferred type of "match" by	herbelin	2010-06-03
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Move from ocamlweb to ocamdoc to generate mli documentation	pboutill	2010-04-29
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Ensures that let-in's in arities of inductive types work well. Maybe not	herbelin	2009-08-11
*	pushed evar reduction in kernel	barras	2009-02-06
*	Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->	herbelin	2008-12-31
*	Prise en compte des coercions dans les clauses "with" même si le type	herbelin	2008-04-23
*	Add the ability to give a transparent_state for conversion, to	msozeau	2008-04-20
*	Changement des named_context	gregoire	2005-12-02
*	compatibility with POWERPC	gregoire	2004-11-22
*	COMMITED BYTECODE COMPILER	barras	2004-10-20
*	Nouvelle en-tête	herbelin	2004-07-16
*	Modules dans COQ\!\!\!\!	coq	2002-08-02
*	nouvel algo de conversion plus uniforme	barras	2001-11-29
*	types vs constr	herbelin	2001-11-20
*	Suites modifs du noyau. Univ devient purement fonctionnel.	barras	2001-11-12
*	GROS COMMIT:	barras	2001-11-05