coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #6820: Tacticals assert_fails and assert_succeeds	Maxime Dénès	2018-03-09
\|\
\| *	Uniform spacing layout in Tactics.v.	Hugo Herbelin	2018-02-28
\| *	Added tacticals assert_succeeds/assert_fails (courtesy of Jason Gross).	Hugo Herbelin	2018-02-28
* \|	Update headers following #6543.	Théo Zimmermann	2018-02-27
\|/
*	Add named timers to LtacProf	Jason Gross	2017-12-14
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Add equality lemmas for sig2 and sigT2	Jason Gross	2017-05-28
*	Add an [inversion_sigma] tactic	Jason Gross	2017-05-28
*	Report a useful error for dependent induction	Tej Chajed	2017-05-03
*	Remove the swap tactic from the prelude.	Maxime Dénès	2016-07-18
*	Giving a more natural semantics to injection by default.	Hugo Herbelin	2016-06-18
*	Update copyright headers.	Maxime Dénès	2016-01-20
*	Reorder the steps of the easy tactic. (Fix for bug #2630)	Guillaume Melquiond	2015-02-25
*	Update headers.	Maxime Dénès	2015-01-12
*	"allows to", like "allowing to", is improper	Jason Gross	2014-08-25
*	Updating headers.	herbelin	2012-08-08
*	induction/destruct : nicer syntax for generating equations (solves #2741)	letouzey	2012-07-09
*	Notation: a new annotation "compat 8.x" extending "only parsing"	letouzey	2012-07-05
*	Modularization of BinNat + fixes of stdlib	letouzey	2011-05-05
*	Fixing an "apply -> ... in hyp" bug (the hyp was considered as a fixed	herbelin	2011-04-28
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Bool: shorter and more systematic proofs + an iff lemma about eqb	letouzey	2010-07-16
*	clear/revert dependent: restrict to hyp(h) instead of ident(h)	letouzey	2010-06-18
*	New tactic "clear dependent", for the moment in ltac in Init/Tactics	letouzey	2010-06-17
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'	letouzey	2009-10-08
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	New tactic to rewrite decidability lemmas when one knows which side	herbelin	2009-08-24
*	Miscellaneous practical commits:	herbelin	2009-06-29
*	- Temptative change to notations like "as [\|n H]_eqn" or "as [\|n H]_eqn:H",	herbelin	2009-01-02
*	- Another bug in get_sort_family_of (sort-polymorphism of constants and	herbelin	2008-12-28
*	- Extracted from the tactic "now" an experimental tactic "easy" for small	herbelin	2008-12-26
*	Correction de bugs:	herbelin	2008-08-05
*	Évolutions diverses et variées.	herbelin	2008-08-04
*	- Extension de "generalize" en "generalize c as id at occs".	herbelin	2008-06-08
*	Ajout notation [ x ; ... ; y ] dans list_scope. Changement de la	herbelin	2008-04-29
*	contradict can now handle False hypothesis in the spirit of contradiction	letouzey	2008-04-09
*	f_equal, revert, specialize in ML, contradict in better Ltac (+doc)	letouzey	2008-03-07
*	Typo	notin	2008-01-23
*	Quelques arguments en plus...	glondu	2007-12-17
*	small tactics "swap" and "absurd_hyp" are now obsolete: "contradict" is	letouzey	2007-11-06
*	Integration of theories/Ints/Z/* in ZArith and large cleanup and extension of...	letouzey	2007-11-06
*	A way to specialize universally quantified hypothesis: if H is	letouzey	2007-11-01
*	Removed an extra \tacindex occurrence for the tactic discriminate.	emakarov	2007-06-08
*	Added back the tactics [apply -> ident], etc. to Tactics.v after	emakarov	2007-04-02
*	Removed the definition of extensions of apply to equivalences	emakarov	2007-04-01
*	Added new tactics for applying equivalences (iff) to Tactics.v:	emakarov	2007-03-30
*	stupid me: ?f two times in a pattern	letouzey	2007-03-26
*	Add f_equal case for 6 arguments.	msozeau	2007-01-02
*	Ajout de la tactique 'remember'	herbelin	2006-10-24