coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Les records déclarés avec Record ne peuvent plus être récursifs (le	aspiwack	2009-01-19
*	- Structuring Numbers and fixing Setoid in stdlib's doc.	herbelin	2009-01-19
*	Getting rid of the previous implementation of setoid_rewrite which was	msozeau	2009-01-18
*	Last changes in type class syntax:	msozeau	2009-01-18
*	DISCLAIMER	puech	2009-01-17
*	Fixing #1960 (xml bug with external on goal variable) and #1961	herbelin	2009-01-14
*	Fixing/improving management of uniform prefix Local and Global	herbelin	2009-01-14
*	- Standardized prefix use of "Local"/"Global" modifiers as decided in	herbelin	2009-01-13
*	Fixing a cosmetic tactic printer bug in passing	herbelin	2009-01-07
*	- Temptative change to notations like "as [\|n H]_eqn" or "as [\|n H]_eqn:H",	herbelin	2009-01-02
*	Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->	herbelin	2008-12-31
*	- Added support for subterm matching in SearchAbout.	herbelin	2008-12-29
*	- Another bug in get_sort_family_of (sort-polymorphism of constants and	herbelin	2008-12-28
*	- coq_makefile: target install now respects the original tree structure	herbelin	2008-12-24
*	Generalized binding syntax overhaul: only two new binders: `() and `{},	msozeau	2008-12-14
*	About "apply in":	herbelin	2008-12-09
*	closed bug 1898: fold x in x; added a reordering primitive tactic	barras	2008-11-26
*	Fixed bug #2006 (type constraint on Record was not taken into account) +	herbelin	2008-11-23
*	Fixed bug in VernacExtend printing + missing vernacular printing rules +	herbelin	2008-11-22
*	Fix mixup between Record, Structure and Class by adding a new variant for	msozeau	2008-11-10
*	Oops... forgot to commit a file related to r11561.	msozeau	2008-11-09
*	More factorization of inductive/record and typeclasses: move class	msozeau	2008-11-09
*	- Fixed bug 1968 (inversion failing due to a Not_found bug introduced in	herbelin	2008-11-09
*	Move Record desugaring to constrintern and add ability to use notations	msozeau	2008-11-05
*	Nouvelle syntaxe pour écrire des records (co)inductifs :	aspiwack	2008-11-05
*	allowed patternidents starting with an '_'	amahboub	2008-10-31
*	The lexer is changer to break former PATTERNIDENT into two tokens.	amahboub	2008-10-30
*	Fixes and refinements regarding occurrence selection:	herbelin	2008-10-26
*	Open notation for declaring record instances.	msozeau	2008-10-23
*	Generalized implementation of generalization.	msozeau	2008-10-23
*	A much better implementation of implicit generalization:	msozeau	2008-10-22
*	Affichage des notations récursives:	herbelin	2008-10-22
*	duplicated open of Ppconstr	letouzey	2008-10-21
*	Renommage "Global Instance" en "Instance Global" pour uniformisation	herbelin	2008-10-20
*	- Export de pattern_ident vers les ARGUMENT EXTEND and co.	herbelin	2008-10-19
*	Report des commits 11417 et 11437 de la v8.2	soubiran	2008-10-15
*	Backporting 11445 from 8.2 to trunk (negative conditions in	herbelin	2008-10-11
*	Add user syntax for creating hint databases [Create HintDb foo	msozeau	2008-09-14
*	Add the ability to declare [Hint Extern]'s with no pattern.	msozeau	2008-09-07
*	Fixes in typeclasses resolution. Avoid reducing instances types before	msozeau	2008-09-07
*	Better handling of the opacity of proof obligations, add the possibility of	msozeau	2008-09-07
*	Report 11364 de 8.2 vers trunk (bugs affichage Print Module)	herbelin	2008-09-05
*	Correct handling of implicit arguments in [Equations] definitions,	msozeau	2008-09-03
*	- Remove some dead code in subtac	msozeau	2008-09-02
*	Propagating commit 11343 from branch v8.2 to trunk (wish 1934 about	herbelin	2008-09-02
*	- New auto hints for transparency/opacity control, not bound to	msozeau	2008-08-22
*	Correction de bugs:	herbelin	2008-08-05
*	Évolutions diverses et variées.	herbelin	2008-08-04
*	Correction d'une incohérence de typage des inductifs polymorphes: les	herbelin	2008-07-25
*	Modification rapide du message d'erreur lorsqu'un _ ne peut être	herbelin	2008-07-18