coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fix checker to handle projections with eta and universe polymorphism correctly.	Matthieu Sozeau	2014-09-06
*	Fix checker treatment of inductives using subst_instances instead of subst_un...	Matthieu Sozeau	2014-09-05
*	Rename eta_expand_ind_stacks, fix the one from the checker and adapt	Matthieu Sozeau	2014-09-05
*	A tentative uniform naming policy in module Inductiveops.	Hugo Herbelin	2014-08-01
*	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
*	Adding a field ci_cstr_nargs to case_info and mind_consnrealargs to	Hugo Herbelin	2014-04-28
*	vi2vo: universes handling finally fixed	Enrico Tassi	2014-03-11
*	checker and votour ported to new vo format (after -vi2vo)	Enrico Tassi	2014-02-26
*	Slightly more compact representation of 'a substituted type,	ppedrot	2013-09-14
*	Change in vo format : digest aren't Marshalled anymore	letouzey	2013-08-22
*	Declarations.mli: reorganization of modular structures	letouzey	2013-08-20
*	State Transaction Machine	gareuselesinge	2013-08-08
*	Checker: vo validation checks the absence of Var/Evar/Meta	letouzey	2013-04-15
*	Checker: vo validation is now done in check.ml (and always)	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