coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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