coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fix checker treatment of inductives using subst_instances instead of subst_un...	Matthieu Sozeau	2014-09-05
*	Removing 'open Univ' from checker.	Pierre-Marie Pédrot	2014-06-07
*	- 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
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Fixing checker with respect to new kernel name structure and hashmaps.	Pierre-Marie Pédrot	2014-03-18
*	vi2vo: universes handling finally fixed	Enrico Tassi	2014-03-11
*	Checker: get rid of code handling section variables	letouzey	2013-04-15
*	Checker: regroup all vo-related types in cic.mli	letouzey	2013-04-15
*	Uniformization of the "anomaly" command.	ppedrot	2013-01-28
*	As r15801: putting everything from Util.array_* to CArray.*.	ppedrot	2012-09-14
*	Noise for nothing	pboutill	2012-03-02
*	Checker/subtyping.ml: avoid adding in env a module already there (fix #2609)	letouzey	2011-10-26
*	More descriptive error messages in checker	glondu	2011-10-20
*	ported r14149 from v8.3 branch: bug in checker (redefined global)	barras	2011-05-23
*	Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks	letouzey	2011-04-03
*	Univ.constraints made fully abstract instead of being a Set of abstract stuff	letouzey	2010-12-18
*	Checker: remove some dead code	letouzey	2010-09-24
*	After the approval of Bruno, here the patch for the checker.	soubiran	2010-04-29
*	This big commit addresses two problems:	soubiran	2009-10-21
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	porting r11900 11905 and 11953 to trunk	barras	2009-03-02
*	added the .vo checker (with independent Makefile)	barras	2008-04-21