coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	library/opaqueTables: enable their use in interactive mode	Enrico Tassi	2014-10-13
*	Grammar: "avoiding to" isn't proper, either	Jason Gross	2014-08-25
*	Initial work on reintroducing old-style polymorphism for compatibility (the s...	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Declarations.mli: reorganization of modular structures	letouzey	2013-08-20
*	Revised infrastructure for lazy loading of opaque proofs	letouzey	2013-04-02
*	kernel/declarations becomes a pure mli	letouzey	2013-02-26
*	Names: revised representation of constants and mutual_inductive	letouzey	2013-02-19
*	Uniformization of the "anomaly" command.	ppedrot	2013-01-28
*	Modulification of Label	ppedrot	2012-12-18
*	Modulification of identifier	ppedrot	2012-12-14
*	Monomorphization (library)	ppedrot	2012-11-22
*	Fixed #2926:	ppedrot	2012-10-29
*	Partial revert of Yann commit in order to use CLib.List when opening	ppedrot	2012-09-14
*	This patch removes unused "open" (automatically generated from	regisgia	2012-09-14
*	Updating headers.	herbelin	2012-08-08
*	Module names and constant/inductive names are now in two separate namespaces	letouzey	2012-03-26
*	Noise for nothing	pboutill	2012-03-02
*	First attempt at making Print Assumption compatible with opaque modules (fix ...	letouzey	2011-10-25