coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Reorganize comment documentation of ChoiceFacts.v	Gaetan Gilbert	2017-05-03
*	Functional choice <-> [inhabited] and [forall] commute	Gaetan Gilbert	2017-04-30
*	Fixing missing PropFacts.v in Logic/vo.itarget.	Hugo Herbelin	2017-03-28
*	Merge PR#392: strengthened the statement of JMeq_eq_dep	Maxime Dénès	2017-03-24
\|\
* \|	Add a forgotten (?) line to "theories/Logic/vo.itarget".	Matej Kosik	2017-03-19
* \|	Merge PR#444: Simplifying a statement in Hurkens.v + a case study for eauto	Maxime Dénès	2017-03-14
\|\ \
* \| \|	Strengthening some of the results in ChoiceFacts.v.	Hugo Herbelin	2017-03-03
* \| \|	Adding explicitly a file to work in the context of propositional extensionality.	Hugo Herbelin	2017-03-03
* \| \|	Adding a file providing extensional choice (i.e. choice over setoids).	Hugo Herbelin	2017-03-03
* \| \|	Adding various properties and characterization of the extensional	Hugo Herbelin	2017-03-03
* \| \|	Slightly unifying renaming in ChoiceFacts.v.	Hugo Herbelin	2017-03-03
* \| \|	Logic library: Adding a characterization of excluded-middle in term of	Hugo Herbelin	2017-03-03
* \| \|	Formatting references with surrounding brackets in Diaconescu.v.	Hugo Herbelin	2017-03-03
\| * \|	Simplifying the proof of NoRetractToModalProposition.paradox in	Hugo Herbelin	2017-02-24
\|/ /
* \|	Fix a typo in Hurkens.v comment	Jason Gross	2016-12-19
\| *	strengthened the statement of JMeq_eq_dep	Abhishek Anand	2016-12-11
\|/
*	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