coq - The formal proof system

Age	Commit message (Expand)	Author
2015-10-28	Avoid type checking private_constants (side_eff) again during Qed (#4357).	Enrico Tassi
2015-09-23	Give a way to control if the decidable-equality schemes are built like	Hugo Herbelin
2015-09-14	Univs: Add universe binding lists to definitions	Matthieu Sozeau
2015-08-02	Reverting 16 last commits, committed mistakenly using the wrong push command.	Hugo Herbelin
2015-08-02	Give a way to control if the decidable-equality schemes are built like	Hugo Herbelin
2015-01-17	Make native compiler handle universe polymorphic definitions.	Maxime Dénès
2015-01-12	Update headers.	Maxime Dénès
2014-08-14	Fix elimschemes accessing directly the universe context of inductives (fixes ...	Matthieu Sozeau
2014-06-18	Proofs now take and return an evar_universe_context, simplifying interfaces	Matthieu Sozeau
2014-06-17	Removing dead code.	Pierre-Marie Pédrot
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2013-08-08	State Transaction Machine	gareuselesinge
2012-10-02	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey
2012-08-08	Updating headers.	herbelin
2011-05-26	Fixing discriminate for identity.	herbelin
2010-09-24	Some dead code removal, thanks to Oug analyzer	letouzey
2010-07-24	Updated all headers for 8.3 and trunk	herbelin
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2009-12-13	Made the side-conditions of lemmas always come last when chaining "apply in"	herbelin