coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fix a typo in Hurkens.v comment	Jason Gross	2016-12-19
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-11-18
\|\
\| *	Remove v62 from stdlib.	Théo Zimmermann	2016-10-24
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-08
\|\\|
\| *	Fixing unexpected "noise" introduced in commit 24d5448c.	Hugo Herbelin	2016-10-06
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-05
\|\\|
\| *	More tests for tactic "subst".	Hugo Herbelin	2016-10-02
* \|	extensionality: Handle dependently-used hypotheses	Jason Gross	2016-09-19
* \|	Adding an "extensionality in H" tactic which applies functional	Hugo Herbelin	2016-09-19
\|/
*	Typo in a comment of stdlib.	Hugo Herbelin	2016-07-08
*	Moving the Tauto tactic to proper Ltac.	Pierre-Marie Pédrot	2016-02-22
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-29
\|\
\| *	Fix bug #4503: mixing universe polymorphic and monomorphic	Matthieu Sozeau	2016-01-23
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\\|
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-17
\|\\|
\| *	Refine tactic now shelves unifiable holes.	Pierre-Marie Pédrot	2015-12-15
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-11
\|\\|
\| *	Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.	Hugo Herbelin	2015-12-10
* \|	Fix to previous commit (ClassicalFacts.v).	Hugo Herbelin	2015-12-05
* \|	Adding proofs on the relation between excluded-middle and minimization.	Hugo Herbelin	2015-12-05
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-29
\|\\|
\| *	Univs: entirely disallow instantiation of polymorphic constants with	Matthieu Sozeau	2015-11-27
* \|	Adding an amazing property of Prop.	Hugo Herbelin	2015-11-07
\|/
*	Minor modifications to WeakFanTheorem.	Hugo Herbelin	2015-09-08
*	Remove some outdated files and fix permissions.	Guillaume Melquiond	2015-07-31
*	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