coq - The formal proof system

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