coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Tentative abbreviation "rew Heq in H" for eq_rect. (feedback welcome)	herbelin	2011-07-16
*	Added a characterization of unique existence.	herbelin	2011-07-16
*	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
*	Made notations for exists, exists! and notations of Utf8.v recursive notations	herbelin	2010-07-22
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Init/Logic: commutativity and associativity of /\ and \/	letouzey	2010-01-08
*	Implicit argument of Logic.eq become maximally inserted	letouzey	2009-10-08
*	Switched to "standardized" names for the properties of eq and	herbelin	2009-01-01
*	- Another bug in get_sort_family_of (sort-polymorphism of constants and	herbelin	2008-12-28
*	- Optimized "auto decomp" which had a (presumably) exponential in	herbelin	2008-12-26
*	Moved several lemmas from theories/Numbers/NumPrelude to theories/Init/Logic.	emakarov	2007-11-08
*	Révision de theories/Logic concernant les axiomes de descriptions.	herbelin	2007-10-03
*	Ajout infos de débogage de "universe inconsistency" quand option Set	herbelin	2007-09-30
*	Mise en forme des theories	notin	2006-10-17