coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	- 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