coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #7690: Fixing typos in file Berardi.v	Pierre-Marie Pédrot	2018-06-05
\|\
* \|	Deprecate implicit tactic solving.	Pierre-Marie Pédrot	2018-06-04
\| *	Fixing typos in file Berardi.v	Hugo Herbelin	2018-06-03
\|/
*	[stdlib] Do not use “Require” inside sections	Vincent Laporte	2018-03-07
*	Merge PR #6855: Update headers following #6543.	Maxime Dénès	2018-03-05
\|\
* \|	Remove the deprecation for some 8.2-8.5 compatibility aliases.	Théo Zimmermann	2018-03-02
\| *	Update headers following #6543.	Théo Zimmermann	2018-02-27
* \|	[stdlib] move “Require” out of sections	Vincent Laporte	2018-02-27
\|/
*	Axiom-free proof of eta expansion.	Jasper Hugunin	2017-12-11
*	Addressing BZ#5713 (classical_left/classical_right artificially restricted).	Hugo Herbelin	2017-09-03
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Remove remaining vo.itarget files (obsolete since PR #499)	Pierre Letouzey	2017-06-10
*	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