coq - The formal proof system

Age	Commit message (Expand)	Author
2014-12-17	checker: Change in library on disk values, now using context_sets instead of	Matthieu Sozeau
2014-12-17	Update checker/values and cic due to changes in case_info and record_body.	Matthieu Sozeau
2014-10-20	A patch for printing "match" when constructors are defined with let-in	Hugo Herbelin
2014-09-06	Fix checker to handle projections with eta and universe polymorphism correctly.	Matthieu Sozeau
2014-09-05	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-08-01	A tentative uniform naming policy in module Inductiveops.	Hugo Herbelin
2014-05-08	Adapt the checker to polymorphic universes and projections (untested).	Matthieu Sozeau
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2014-04-28	Adding a field ci_cstr_nargs to case_info and mind_consnrealargs to	Hugo Herbelin
2014-03-11	vi2vo: universes handling finally fixed	Enrico Tassi
2014-02-26	checker and votour ported to new vo format (after -vi2vo)	Enrico Tassi
2013-09-14	Slightly more compact representation of 'a substituted type,	ppedrot
2013-08-22	Change in vo format : digest aren't Marshalled anymore	letouzey
2013-08-20	Declarations.mli: reorganization of modular structures	letouzey
2013-08-08	State Transaction Machine	gareuselesinge
2013-04-15	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