coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	A new version of Hurkens.v.	Arnaud Spiwack	2014-09-24
*	Prove forall extensionality	Jason Gross	2014-08-26
*	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
*	Added a (constructive) proof of Weak Konig's lemma for decidable trees.	Hugo Herbelin	2014-07-15
*	Some basics facts about eq_dep.	Hugo Herbelin	2014-07-15
*	Remove some theories that have been deprecated for 10 years.	Guillaume Melquiond	2014-06-26
*	Making those proofs which depend on names generated for the arguments	Hugo Herbelin	2014-06-01
*	- 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
*	Correct rebase on STM code. Thanks to E. Tassi for help on dealing with	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Closing bug #3164	Julien Forest	2014-04-04
*	fixup complement Fin	Pierre Boutillier	2014-02-24
*	FinFun.v: results about injective/surjective/bijective fonctions over finite ...	Pierre Letouzey	2014-02-07
*	Generalize eq_proofs_unicity	Jason Gross	2013-12-12
*	Improved the presentation of the proof of UIP_refl_nat.	Hugo Herbelin	2013-12-04
*	Adding a dependent version of equal_f, thus fixing #3074.	ppedrot	2013-08-02
*	A constructive proof of Fan theorem where paths are represented by predicates.	herbelin	2013-06-02
*	Unset Asymmetric Patterns	pboutill	2013-01-18
*	Making subset_eq_compat applying over more general domain "Type" (see #2938).	herbelin	2012-12-05
*	Identities over types satisfying Uniqueness of Identity Proofs	herbelin	2012-12-04
*	Isolating the ingredients of the proof of Prop<>Type (r15973). Seeing	herbelin	2012-11-15
*	Added a proof that Prop<>Type, for arbitrary fixed Type.	herbelin	2012-11-15
*	A decidability property of functional relations over decidable codomains.	herbelin	2012-11-15
*	For the record, two examples of short proofs of uniqueness of identity	herbelin	2012-11-15
*	Updating headers.	herbelin	2012-08-08
*	Kills the useless tactic annotations "in \|- *"	letouzey	2012-07-05
*	Open Local Scope ---> Local Open Scope, same with Notation and alii	letouzey	2012-07-05
*	ZArith + other : favor the use of modern names instead of compat notations	letouzey	2012-07-05
*	Intuition: temporary(?) restore the unconditional unfolding of not	letouzey	2012-05-15
*	remove undocumented and scarcely-used tactic auto decomp	letouzey	2012-04-23
*	theories/, plugins/ and test-suite/ ported to the Arguments vernacular	gareuselesinge	2011-11-21
*	Cleaning a little bit the files talking about descriptions: avoiding	herbelin	2011-11-03
*	Removing vernacular code mistakenly committed.	herbelin	2011-10-05
*	Use of the standard terminology for Diaconescu's theorem (not "paradox").	herbelin	2011-08-23
*	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
*	Some facts about functional extensionality (especially alternative	herbelin	2011-07-16
*	More lemmas relating the different equivalent formulations of eq_dep.	herbelin	2011-07-16
*	First release of Vector library.	pboutill	2010-12-10
*	Used multiple lists of implicit arguments to transfer the choices of	herbelin	2010-10-23
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Made notations for exists, exists! and notations of Utf8.v recursive notations	herbelin	2010-07-22
*	Backported r13308 (ConstructiveEpsilon.v) to branch v8.3	herbelin	2010-07-22
*	Update of ConstructiveEpsilon.v by Jean-François Monin.	herbelin	2010-07-22
*	Tentative fix for bug #2226: put inj_pair2 and eq_dep_eq hints in a	msozeau	2010-06-09
*	Made option "Automatic Introduction" active by default before too many	herbelin	2010-06-08