coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #6743: Add notation {x & P} for sigT	Maxime Dénès	2018-03-08
\|\
* \	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
\|/ /
* \|	Trying a hack to support {'pat\|P} without breaking compatibility.	Hugo Herbelin	2018-02-20
* \|	Adding notations of the form "{'pat\|P}", "exists2 'pat, P & Q", etc.	Hugo Herbelin	2018-02-20
\| *	Add notation {x & P} for sigT	Tej Chajed	2018-02-12
\|/
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	More uniform indentation of sigma lemmas	Jason Gross	2017-05-28
*	Give explicit proof terms to proj2_sig_eq etc.	Jason Gross	2017-05-28
*	Add some more comments about sigma equalities	Jason Gross	2017-05-28
*	Remove motive argument from [rew dependent]	Jason Gross	2017-05-28
*	Use a local [rew dependent] notation	Jason Gross	2017-05-28
*	Add forward-chaining versions: [eq_sig*_uncurried]	Jason Gross	2017-05-28
*	Use notation for sigT	Jason Gross	2017-05-28
*	Remove reference to [IsIso]	Jason Gross	2017-05-28
*	Use notations for [sig], [sigT], [sig2], [sigT2]	Jason Gross	2017-05-28
*	Use [rew_] instead of [eq_rect_] prefix	Jason Gross	2017-05-28
*	Add equality lemmas for sig2 and sigT2	Jason Gross	2017-05-28
*	Use [rew] notations rather than [eq_rect]	Jason Gross	2017-05-28
*	Add lemmas about equality of sigma types	Jason Gross	2017-05-28
*	Functional choice <-> [inhabited] and [forall] commute	Gaetan Gilbert	2017-04-30
*	Add η principles for sigma types	Jason Gross	2017-03-01
*	Remove some trailing whitespace in Init/Specif.v	Jason Gross	2017-03-01
*	Remove v62 from stdlib.	Théo Zimmermann	2016-10-24
*	Adding option "Set Reversible Pattern Implicit" to Specif.v so that an	Hugo Herbelin	2016-06-16
*	Revert "Adding option "Set Reversible Pattern Implicit" to Specif.v so that an"	Hugo Herbelin	2016-04-27
*	Adding option "Set Reversible Pattern Implicit" to Specif.v so that an	Hugo Herbelin	2016-04-27
*	Update copyright headers.	Maxime Dénès	2016-01-20
*	Reverting 16 last commits, committed mistakenly using the wrong push command.	Hugo Herbelin	2015-08-02
*	Adding a notation { x & P } for { x : _ & P }.	Hugo Herbelin	2015-08-02
*	Correct restriction of vm_compute when handling universe polymorphic	Matthieu Sozeau	2015-01-15
*	Update headers.	Maxime Dénès	2015-01-12
*	- Fix printing and parsing of primitive projections, including the Set	Matthieu Sozeau	2014-09-09
*	- Fix bug preventing apply from unfolding Fixpoints.	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	No more Coersion in Init.	Pierre Boutillier	2014-04-10
*	Define [projT3] and [proj3_sig]	Jason Gross	2014-04-10
*	Better unification for [projT1] and [proj1_sig].	Jason Gross	2013-12-12
*	Relaxing the constraint on eta-expanding on the fly while looking for	herbelin	2013-05-05
*	Unset Asymmetric Patterns	pboutill	2013-01-18
*	Updating headers.	herbelin	2012-08-08
*	ZArith + other : favor the use of modern names instead of compat notations	letouzey	2012-07-05
*	Bug 2767	pboutill	2012-05-09
*	theories/, plugins/ and test-suite/ ported to the Arguments vernacular	gareuselesinge	2011-11-21
*	Same Implicit Arguments rule for sumbool and sumor.	pboutill	2011-07-26
*	Init: some results in Type should rather be Defined than Qed	letouzey	2011-03-21
*	Used multiple lists of implicit arguments to transfer the choices of	herbelin	2010-10-23
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29