coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
* \|	Fixing some problems with double induction.	Hugo Herbelin	2016-01-21
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
\|/
*	Update headers.	Maxime Dénès	2015-01-12
*	Preserving the good effect of 014e5ac92a on not leaving dangling local	Hugo Herbelin	2014-11-14
*	Compatibility with 8.4 in the heuristic used to build the induction	Hugo Herbelin	2014-11-08
*	Some reorganization of the code for destruct/induction:	Hugo Herbelin	2014-11-02
*	This commit introduces changes in induction and destruct.	Hugo Herbelin	2014-10-25
*	Synchronized names from the "as" clause with the skeleton of the	Hugo Herbelin	2014-06-30
*	Updating headers.	herbelin	2012-08-08
*	Restore test file induct.v where the "in \|- *" is mandatory	letouzey	2012-07-10
*	Kills the useless tactic annotations "in \|- *"	letouzey	2012-07-05
*	"Let in" in pattern hell, one more iteration	pboutill	2012-03-02
*	Added support for referring to subterms of the goal by pattern.	herbelin	2011-09-26
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Fixed two tests that was incorrectly typed in former revisions 12348 and 12356.	herbelin	2009-09-27
*	Only one "in" clause in "destruct" even for a multiple "destruct".	herbelin	2009-09-20
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Ensures that let-in's in arities of inductive types work well. Maybe not	herbelin	2009-08-11
*	Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8	herbelin	2005-12-21
*	Nouvelle en-tête	herbelin	2004-07-16
*	entetes	filliatr	2001-03-15
*	Ajout de tests	mohring	2000-12-12