coq - The formal proof system

Age	Commit message (Expand)	Author
2015-11-04	Checker was forgetting to register global universes introduced by opaque	Matthieu Sozeau
2014-02-26	checker and votour ported to new vo format (after -vi2vo)	Enrico Tassi
2013-10-24	Rtree : cleanup of the comparing code	letouzey
2013-08-20	Declarations.mli: reorganization of modular structures	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-02	Revised infrastructure for lazy loading of opaque proofs	letouzey
2013-02-12	Checker: re-sync vo structures after Maxime's commit 16136	letouzey
2012-12-18	Modulification of mod_bound_id	ppedrot
2012-12-14	Modulification of identifier	ppedrot
2012-05-29	remove many excessive open Util & Errors in mli's	letouzey
2012-03-02	Noise for nothing	pboutill
2011-04-03	Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks	letouzey
2011-01-31	A fine-grain control of inlining at functor application via priority levels	letouzey
2010-09-24	Checker: remove some dead code	letouzey
2010-07-30	adpated the checker to handle coomutative cuts and lazyness	barras
2010-04-29	After the approval of Bruno, here the patch for the checker.	soubiran
2010-02-19	added validation of delta_resolver (which seem to have an impact on typing)	barras
2009-10-21	This big commit addresses two problems:	soubiran
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-08-22	Transfers to checker ("let"s in inductive arities + Coq root read-only).	herbelin
2009-03-02	porting r11900 11905 and 11953 to trunk	barras
2008-10-15	Report des commits 11417 et 11437 de la v8.2	soubiran
2008-05-07	fixed bug with aliases	barras
2008-05-06	checker deals with polymorphic constants and module aliases	barras
2008-04-21	added the .vo checker (with independent Makefile)	barras