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
\|/
*	Fix typo in documentation for identity	Tej Chajed	2017-07-05
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Give andb_prop a simpler proof	Jason Gross	2017-04-25
*	A couple of other useful properties about compare_cont.	Hugo Herbelin	2017-03-03
*	Compatibility of iff wrt not and imp.	Hugo Herbelin	2017-03-03
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	Tentatively setting cons and Some with 1st implicit argument maximal	Hugo Herbelin	2015-05-09
* \|	Correct restriction of vm_compute when handling universe polymorphic	Matthieu Sozeau	2015-01-18
\| *	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
*	Try a new way of handling template universe levels	Matthieu Sozeau	2014-05-06
*	- 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
*	[Coercion]s use [Sortclass], not [Prop] (in docs)	Jason Gross	2014-01-24
*	Updating headers.	herbelin	2012-08-08
*	Kills the useless tactic annotations "in \|- *"	letouzey	2012-07-05
*	ZArith + other : favor the use of modern names instead of compat notations	letouzey	2012-07-05
*	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
*	Arithemtic: more concerning compare, eqb, leb, ltb	letouzey	2011-06-20
*	Modularization of BinNat + fixes of stdlib	letouzey	2011-05-05
*	Better comments and organisation in Datatypes.v	letouzey	2011-05-05
*	Init: some results in Type should rather be Defined than Qed	letouzey	2011-03-21
*	CompareSpec: a slight generalization/reformulation of CompSpec	letouzey	2011-03-17
*	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
*	Bool: iff lemmas about or, a reflect inductive, an is_true function	letouzey	2010-07-10
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	CompSpec2Type is used to build functions, it should be Defined, not Qed	letouzey	2010-02-13
*	CompSpecType, a clone of CompSpec but in Type instead of Prop	letouzey	2010-02-12
*	Datatypes.length and app defined back via fun+fix instead of Fixpoint	letouzey	2009-11-06
*	Better visibility of the inductive CompSpec used to specify comparison functions	letouzey	2009-11-03
*	list, length, app are migrated from List to Datatypes	letouzey	2009-11-02
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	OrderedTypeEx.N_as_OT use Nlt, various minor improvements in N/ZArith	letouzey	2009-07-24
*	Miscellaneous practical commits:	herbelin	2009-06-29
*	Parsing files for numerals (+ ascii/string) moved into plugins	letouzey	2009-03-27
*	Switched to "standardized" names for the properties of eq and	herbelin	2009-01-01
*	- Optimized "auto decomp" which had a (presumably) exponential in	herbelin	2008-12-26
*	Fine-tuning rewriting from "eq_true b": using <- to rewrite true to b	herbelin	2008-11-23
*	- Fixed minor bug #1994 in the tactic chapter of the manual [doc]	herbelin	2008-11-22
*	- Patch sur "intros until 0"	herbelin	2008-06-08
*	Notation concise pour la valeur par défaut des cas reconnus comme	herbelin	2008-05-28
*	Added the automatic generation of the boolean equality if possible and the	vsiles	2007-10-05
*	Déplacement des opérations sur bool dans l'état initial	herbelin	2007-04-28