coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	- Temptative change to notations like "as [\|n H]_eqn" or "as [\|n H]_eqn:H",	herbelin	2009-01-02
*	Switched to "standardized" names for the properties of eq and	herbelin	2009-01-01
*	- 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
*	- Optimized "auto decomp" which had a (presumably) exponential in	herbelin	2008-12-26
*	Fine-tuning rewriting from "eq_true b": using <- to rewrite true to b	herbelin	2008-11-23
*	- Fixed minor bug #1994 in the tactic chapter of the manual [doc]	herbelin	2008-11-22
*	ugly comment erroneously left in the minus definition	letouzey	2008-10-14
*	Correction de bugs:	herbelin	2008-08-05
*	Évolutions diverses et variées.	herbelin	2008-08-04
*	Fixed doc of inductive sort-polymorphism (cf bug #1908). Seized the	herbelin	2008-07-23
*	Changing the definitions of pred and minus in the style of GG	werner	2008-06-12
*	- Patch sur "intros until 0"	herbelin	2008-06-08
*	- Extension de "generalize" en "generalize c as id at occs".	herbelin	2008-06-08
*	Petites corrections diverses :	herbelin	2008-06-02
*	- Modification de la déf de minus et pred conformément aux remarques de	herbelin	2008-05-28
*	Notation concise pour la valeur par défaut des cas reconnus comme	herbelin	2008-05-28
*	MAJ et bricoles diverses	herbelin	2008-05-12
*	Backtrack sur la mise à disposition en standard de la notation [ x ; ... ; y ]	herbelin	2008-05-09
*	Ajout notation [ x ; ... ; y ] dans list_scope. Changement de la	herbelin	2008-04-29
*	Prise en compte des coercions dans les clauses "with" même si le type	herbelin	2008-04-23
*	contradict can now handle False hypothesis in the spirit of contradiction	letouzey	2008-04-09
*	Nettoyage Wf.v et unification (suite remarques faites sur cocorico)	herbelin	2008-03-23
*	Une passe sur les réels:	herbelin	2008-03-23
*	Do a second pass on the treatment of user-given implicit arguments. Now	msozeau	2008-03-15
*	f_equal, revert, specialize in ML, contradict in better Ltac (+doc)	letouzey	2008-03-07
*	still one more substituion s/Set/Type/	letouzey	2008-03-04
*	Proper implicit arguments handling for assumptions	msozeau	2008-02-26
*	Typo	notin	2008-01-23
*	Quelques arguments en plus...	glondu	2007-12-17
*	Moved several lemmas from theories/Numbers/NumPrelude to theories/Init/Logic.	emakarov	2007-11-08
*	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
*	Added the automatic generation of the boolean equality if possible and the	vsiles	2007-10-05
*	Révision de theories/Logic concernant les axiomes de descriptions.	herbelin	2007-10-03
*	Ajout infos de débogage de "universe inconsistency" quand option Set	herbelin	2007-09-30
*	Fix dependency bugs due to Program modules renamings.	msozeau	2007-08-08
*	Move Program tactics into a proper theories/ directory as they are general pu...	msozeau	2007-08-07
*	Ajout exist & cie à la table des hints par symétrie avec ex_intro &	herbelin	2007-06-22
*	Removed an extra \tacindex occurrence for the tactic discriminate.	emakarov	2007-06-08
*	Gestion espaces dans notation _ = _ :> _	herbelin	2007-06-05
*	Déplacement des opérations sur bool dans l'état initial	herbelin	2007-04-28
*	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
*	Mise en forme des theories	notin	2006-10-17