coq - The formal proof system

Age	Commit message (Expand)	Author
2016-07-18	Remove the swap tactic from the prelude.	Maxime Dénès
2016-06-18	Giving a more natural semantics to injection by default.	Hugo Herbelin
2016-01-20	Update copyright headers.	Maxime Dénès
2015-02-25	Reorder the steps of the easy tactic. (Fix for bug #2630)	Guillaume Melquiond
2015-01-12	Update headers.	Maxime Dénès
2014-08-25	"allows to", like "allowing to", is improper	Jason Gross
2012-08-08	Updating headers.	herbelin
2012-07-09	induction/destruct : nicer syntax for generating equations (solves #2741)	letouzey
2012-07-05	Notation: a new annotation "compat 8.x" extending "only parsing"	letouzey
2011-05-05	Modularization of BinNat + fixes of stdlib	letouzey
2011-04-28	Fixing an "apply -> ... in hyp" bug (the hyp was considered as a fixed	herbelin
2010-07-24	Updated all headers for 8.3 and trunk	herbelin
2010-07-16	Bool: shorter and more systematic proofs + an iff lemma about eqb	letouzey
2010-06-18	clear/revert dependent: restrict to hyp(h) instead of ident(h)	letouzey
2010-06-17	New tactic "clear dependent", for the moment in ltac in Init/Tactics	letouzey
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2009-10-08	Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'	letouzey
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-08-24	New tactic to rewrite decidability lemmas when one knows which side	herbelin
2009-06-29	Miscellaneous practical commits:	herbelin
2009-01-02	- Temptative change to notations like "as [\|n H]_eqn" or "as [\|n H]_eqn:H",	herbelin
2008-12-28	- Another bug in get_sort_family_of (sort-polymorphism of constants and	herbelin
2008-12-26	- Extracted from the tactic "now" an experimental tactic "easy" for small	herbelin
2008-08-05	Correction de bugs:	herbelin
2008-08-04	Évolutions diverses et variées.	herbelin
2008-06-08	- Extension de "generalize" en "generalize c as id at occs".	herbelin
2008-04-29	Ajout notation [ x ; ... ; y ] dans list_scope. Changement de la	herbelin
2008-04-09	contradict can now handle False hypothesis in the spirit of contradiction	letouzey
2008-03-07	f_equal, revert, specialize in ML, contradict in better Ltac (+doc)	letouzey
2008-01-23	Typo	notin
2007-12-17	Quelques arguments en plus...	glondu
2007-11-06	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-01	A way to specialize universally quantified hypothesis: if H is	letouzey
2007-06-08	Removed an extra \tacindex occurrence for the tactic discriminate.	emakarov
2007-04-02	Added back the tactics [apply -> ident], etc. to Tactics.v after	emakarov
2007-04-01	Removed the definition of extensions of apply to equivalences	emakarov
2007-03-30	Added new tactics for applying equivalences (iff) to Tactics.v:	emakarov
2007-03-26	stupid me: ?f two times in a pattern	letouzey
2007-01-02	Add f_equal case for 6 arguments.	msozeau
2006-10-24	Ajout de la tactique 'remember'	herbelin
2006-10-05	revision de la semantique de rewrite ... in <clause>. details dans la doc	letouzey
2006-09-22	Ajout d'une valeur VList dans tacinterp pour permettre de cabler des	herbelin
2006-09-21	incomplete and temporary fix for PR#1222: revert accepts up to 10 args	letouzey
2006-02-27	quelques raccourcis commodes + un f_equal plus efficace	letouzey
2005-08-26	* empty log message *	letouzey
2005-05-17	Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...	herbelin
2005-02-23	quelques tactics ltac	letouzey
2005-02-03	Nouveau fichier Tactics.v collectant les tactiques utiles des utilisateurs	herbelin