coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Update headers.	Maxime Dénès	2015-01-12
*	Added an arithmetical characterization of the hypothesis of WKL.	Hugo Herbelin	2014-12-01
*	Improving elimination with indices, getting rid of intrusive residual	Hugo Herbelin	2014-11-02
*	Make sure that Logic/ExtensionalityFacts gets compiled.	Guillaume Melquiond	2014-10-27
*	Fix some typos.	Guillaume Melquiond	2014-10-27
*	Fix some typos in comments.	Guillaume Melquiond	2014-10-27
*	EqdepFacts: generalize statements which were wrongly restricted to Prop.	Arnaud Spiwack	2014-10-22
*	ConstructiveEpsilon: simplify the before_witness type using non-uniform param...	Arnaud Spiwack	2014-10-16
*	Hurkens.v: Fix a syntax error.	Arnaud Spiwack	2014-09-26
*	ClassicalFacts: adds a proof that weak excluded middle implies weak proof irr...	Arnaud Spiwack	2014-09-26
*	Hurkens.v: new paradox: type of modal propositions is not a retract.	Arnaud Spiwack	2014-09-26
*	Hurkens.v: fix coqdoc formatting in a comment.	Arnaud Spiwack	2014-09-26
*	Hurkens.v: update comments.	Arnaud Spiwack	2014-09-25
*	Return a Prop not an arbitrary Type, and correct a typo.	Matthieu Sozeau	2014-09-24
*	Hurkens.v: show proofs in coqdoc.	Arnaud Spiwack	2014-09-24
*	Hurkens.v: a proof of [Type@{i}<>A] for any [A:Type@{i}].	Arnaud Spiwack	2014-09-24
*	Hurkens.v: coqdoc documentation.	Arnaud Spiwack	2014-09-24
*	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