coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	[api] Deprecate all legacy uses of Names in core.	Emilio Jesus Gallego Arias	2017-11-06
*	Fixing the checker w.r.t. wrongly used abstract universe contexts.	Pierre-Marie Pédrot	2017-07-19
*	Correct coqchk reduction	Amin Timany	2017-06-16
*	Moving unused code out of the kernel into Termops.	Pierre-Marie Pédrot	2016-10-31
*	CLEANUP: Simplifying the changes done in "checker/*"	Matej Kosik	2016-02-15
*	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-09
*	Remove unused substitution functions in checker.	Matthieu Sozeau	2014-09-05
*	Fix checker treatment of inductives using subst_instances instead of subst_un...	Matthieu Sozeau	2014-09-05
*	- Force every universe level to be >= Prop, so one cannot "go under" it anymore.	Matthieu Sozeau	2014-06-04
*	Adapt the checker to polymorphic universes and projections (untested).	Matthieu Sozeau	2014-05-08
*	More monomorphic List.mem + List.assoc + ...	letouzey	2013-10-24
*	Checker: get rid of code handling section variables	letouzey	2013-04-15
*	Checker: empty sections hardcoded in cb and mind	letouzey	2013-04-15
*	Checker: reified encoding of .vo types in values.ml	letouzey	2013-04-15
*	Checker: regroup all vo-related types in cic.mli	letouzey	2013-04-15
*	Checker: re-sync vo structures after Maxime's commit 16136	letouzey	2013-02-12
*	Modulification of identifier	ppedrot	2012-12-14
*	Checker: remove some dead code	letouzey	2010-09-24
*	adpated the checker to handle coomutative cuts and lazyness	barras	2010-07-30
*	fixed confusion between number of cstr arguments and number of pattern variab...	barras	2010-03-12
*	porting r11900 11905 and 11953 to trunk	barras	2009-03-02
*	fixed dependency problems with the checker	barras	2008-05-22