coq - The formal proof system

Age	Commit message (Expand)	Author
2016-01-23	Fix bug #4503: mixing universe polymorphic and monomorphic	Matthieu Sozeau
2016-01-20	Update copyright headers.	Maxime Dénès
2015-12-15	Refine tactic now shelves unifiable holes.	Pierre-Marie Pédrot
2015-12-10	Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.	Hugo Herbelin
2015-11-27	Univs: entirely disallow instantiation of polymorphic constants with	Matthieu Sozeau
2015-09-08	Minor modifications to WeakFanTheorem.	Hugo Herbelin
2015-07-31	Remove some outdated files and fix permissions.	Guillaume Melquiond
2015-01-12	Update headers.	Maxime Dénès
2014-12-01	Added an arithmetical characterization of the hypothesis of WKL.	Hugo Herbelin
2014-11-02	Improving elimination with indices, getting rid of intrusive residual	Hugo Herbelin
2014-10-27	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-22	EqdepFacts: generalize statements which were wrongly restricted to Prop.	Arnaud Spiwack
2014-10-16	ConstructiveEpsilon: simplify the before_witness type using non-uniform param...	Arnaud Spiwack
2014-09-26	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-25	Hurkens.v: update comments.	Arnaud Spiwack
2014-09-24	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-08-26	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-25	"allows to", like "allowing to", is improper	Jason Gross
2014-07-17	Completing c236b51348d2 by fixing EqdepFactsv actually committing the	Hugo Herbelin
2014-07-15	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-06-26	Remove some theories that have been deprecated for 10 years.	Guillaume Melquiond
2014-06-01	Making those proofs which depend on names generated for the arguments	Hugo Herbelin
2014-05-06	- 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-04-04	Closing bug #3164	Julien Forest
2014-02-24	fixup complement Fin	Pierre Boutillier
2014-02-07	FinFun.v: results about injective/surjective/bijective fonctions over finite ...	Pierre Letouzey
2013-12-12	Generalize eq_proofs_unicity	Jason Gross
2013-12-04	Improved the presentation of the proof of UIP_refl_nat.	Hugo Herbelin
2013-08-02	Adding a dependent version of equal_f, thus fixing #3074.	ppedrot
2013-06-02	A constructive proof of Fan theorem where paths are represented by predicates.	herbelin
2013-01-18	Unset Asymmetric Patterns	pboutill
2012-12-05	Making subset_eq_compat applying over more general domain "Type" (see #2938).	herbelin
2012-12-04	Identities over types satisfying Uniqueness of Identity Proofs	herbelin
2012-11-15	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