coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Swapping Context and Constr: defining declarations on constr in Constr.	Hugo Herbelin	2018-06-27
*	Fix #7333: vm_compute segfaults / Anomaly with cofix	Maxime Dénès	2018-05-28
*	Remove vm_conv hook and reorganize kernel files	Maxime Dénès	2018-05-28
*	Cumulativity: improve treatment of irrelevant universes.	Gaëtan Gilbert	2018-03-09
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
*	Merge PR #1082: Fixing Print for inductive types with let-in in parameters	Maxime Dénès	2018-02-12
\|\
* \|	Use specialized function for inductive subtyping inference.	Gaëtan Gilbert	2018-02-11
* \|	Simplification: cumulativity information is variance information.	Gaëtan Gilbert	2018-02-10
* \|	[get_cumulativity_constraints] allowing further code sharing.	Gaëtan Gilbert	2018-02-10
* \|	Factorize code for comparing maybe-cumulative inductives.	Gaëtan Gilbert	2018-02-10
\| *	Fixing a bug of Print for inductive types with let-ins in parameters.	Hugo Herbelin	2017-12-14
\|/
*	[api] Remove yet another type alias.	Emilio Jesus Gallego Arias	2017-12-09
*	[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
*	Fix bugs and add an option for cumulativity	Amin Timany	2017-06-16
*	Use inductive subtyping for conv/cumul	Amin Timany	2017-06-16
*	Univs: fix bug #5180	Matthieu Sozeau	2016-11-30
*	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