coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
\|/
*	Adding notations of the form "{'pat\|P}", "exists2 'pat, P & Q", etc.	Hugo Herbelin	2018-02-20
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Use the rew dependent notation in ex, ex2 proofs	Jason Gross	2017-05-28
*	Make theorems about ex equality Qed	Jason Gross	2017-05-28
*	Make new proofs of equality Qed	Jason Gross	2017-05-28
*	Use extended notation for ex, ex2 types	Jason Gross	2017-05-28
*	Replace [ex'] with [ex]	Jason Gross	2017-05-28
*	Use [rew_] instead of [eq_rect_] prefix	Jason Gross	2017-05-28
*	Add lemmas for ex2	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
*	Use [rew_] instead of [eq_rect_] prefix	Jason Gross	2017-05-28
*	Use [rew] notations rather than [eq_rect]	Jason Gross	2017-05-28
*	Add more groupoid-like theorems about [eq]	Jason Gross	2017-05-28
*	Functional choice <-> [inhabited] and [forall] commute	Gaetan Gilbert	2017-04-30
*	Small typo in comment	Vadim Zaliva	2017-04-26
*	Merge branch 'v8.6' into trunk	Maxime Dénès	2017-04-15
\|\
* \	Merge PR#442: Allow interactive editing of Coq.Init.Logic	Maxime Dénès	2017-03-17
\|\ \
* \| \|	Compatibility of iff wrt not and imp.	Hugo Herbelin	2017-03-03
\| \| *	Fixing a little bug in printing ex2 (type was printed "_" by default).	Hugo Herbelin	2017-02-23
\| \|/ \|/\|
\| *	Allow interactive editing of Coq.Init.Logic	Jason Gross	2017-02-21
\|/
*	Update copyright headers.	Maxime Dénès	2016-01-20
*	Remove Print Universe directive.	Matthieu Sozeau	2015-10-02
*	Universes: enforce Set <= i for all Type occurrences.	Matthieu Sozeau	2015-10-02
*	admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)	Enrico Tassi	2015-03-11
*	Update headers.	Maxime Dénès	2015-01-12
*	Improving elimination with indices, getting rid of intrusive residual	Hugo Herbelin	2014-11-02
*	Supporting "at occs" as a short-hand for "in \|- * at occs" in "destruct".	Hugo Herbelin	2014-11-02
*	Basic lemmas about the algebraic structure of equality.	Hugo Herbelin	2014-05-31
*	Removing comment outdated since eta holds in conversion rule (this	Hugo Herbelin	2014-05-07
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Side effect free implementation of admit (Isabelle's oracle)	gareuselesinge	2013-08-08
*	Improving printing of 'rew' notation	herbelin	2013-05-05
*	Added group properties of eq_refl, eq_sym, eq_trans	herbelin	2013-04-17
*	Some lemmas on property of rewriting. It will probably be worth at	herbelin	2012-11-15
*	Removed a few calls to "Opaque" in Logic.v ineffective since at least	herbelin	2012-10-24
*	Updating headers.	herbelin	2012-08-08
*	Kills the useless tactic annotations "in \|- *"	letouzey	2012-07-05
*	Notation: a new annotation "compat 8.x" extending "only parsing"	letouzey	2012-07-05
*	"A -> B" is a notation for "forall _ : A, B".	pboutill	2012-04-12
*	Fixing a few bugs (see #2571) related to interpretation of multiple binders	herbelin	2012-04-06
*	No more use of tauto in Init/	pboutill	2012-01-19
*	theories/, plugins/ and test-suite/ ported to the Arguments vernacular	gareuselesinge	2011-11-21
*	Take benefit of bullets available by default in Prelude	herbelin	2011-08-10
*	Less ambitious application of a notation for eq_rect. We proposed	herbelin	2011-08-10
*	New proposition "rewrite Heq in H" for eq_rect (assuming that there is	herbelin	2011-08-08
*	All the parameters of or can be implicits.	pboutill	2011-07-26