coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	revision de la semantique de rewrite ... in <clause>. details dans la doc	letouzey	2006-10-05
*	Ajout d'une valeur VList dans tacinterp pour permettre de cabler des	herbelin	2006-09-22
*	incomplete and temporary fix for PR#1222: revert accepts up to 10 args	letouzey	2006-09-21
*	quelques raccourcis commodes + un f_equal plus efficace	letouzey	2006-02-27
*	* empty log message *	letouzey	2005-08-26
*	Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...	herbelin	2005-05-17
*	quelques tactics ltac	letouzey	2005-02-23
*	Nouveau fichier Tactics.v collectant les tactiques utiles des utilisateurs	herbelin	2005-02-03