coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Typo in a comment of stdlib.	Hugo Herbelin	2016-07-08
*	Update copyright headers.	Maxime Dénès	2016-01-20
*	Update headers.	Maxime Dénès	2015-01-12
*	Improving elimination with indices, getting rid of intrusive residual	Hugo Herbelin	2014-11-02
*	EqdepFacts: generalize statements which were wrongly restricted to Prop.	Arnaud Spiwack	2014-10-22
*	Return a Prop not an arbitrary Type, and correct a typo.	Matthieu Sozeau	2014-09-24
*	sed s'/_one_var/_on/g'	Jason Gross	2014-08-26
*	Generalize EqdepFacts	Jason Gross	2014-08-26
*	"allows to", like "allowing to", is improper	Jason Gross	2014-08-25
*	Completing c236b51348d2 by fixing EqdepFactsv actually committing the	Hugo Herbelin	2014-07-17
*	Some basics facts about eq_dep.	Hugo Herbelin	2014-07-15
*	- Fix bug preventing apply from unfolding Fixpoints.	Matthieu Sozeau	2014-05-06
*	Adapt universe polymorphic branch to new handling of futures for delayed proofs.	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Identities over types satisfying Uniqueness of Identity Proofs	herbelin	2012-12-04
*	Updating headers.	herbelin	2012-08-08
*	ZArith + other : favor the use of modern names instead of compat notations	letouzey	2012-07-05
*	theories/, plugins/ and test-suite/ ported to the Arguments vernacular	gareuselesinge	2011-11-21
*	Less ambitious application of a notation for eq_rect. We proposed	herbelin	2011-08-10
*	New proposition "rewrite Heq in H" for eq_rect (assuming that there is	herbelin	2011-08-08
*	More lemmas relating the different equivalent formulations of eq_dep.	herbelin	2011-07-16
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Added a few informations about file lineages (for the most part in kernel)	herbelin	2010-05-09
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Fix the stdlib doc compilation + switch all .v file to utf8	letouzey	2009-09-28
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	- Optimized "auto decomp" which had a (presumably) exponential in	herbelin	2008-12-26
*	- Amélioration nommage dans EqdepFacts suivant remarque de Arthur C.	herbelin	2008-06-10
*	Révision de theories/Logic concernant les axiomes de descriptions.	herbelin	2007-10-03
*	Passage de Set à Type dans Relations et Wellfounded	herbelin	2007-02-06
*	Correction typo eq_rec_eq (cf bug #1339)	herbelin	2007-01-31
*	Mise en forme des theories	notin	2006-10-17
*	Réajout de eq_rec_eq oublié lors de la modularisation de Eqdep	herbelin	2006-03-30
*	Modularisation des preuves concernant la logique classique, l'indiscernabilit...	herbelin	2006-03-05