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
*	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
*	fixed indentation of subgoals for Show Script	barras	2008-07-17
*	Uniformisation du format des messages d'erreur (commencent par une	herbelin	2008-07-17
*	Autour du parsing:	herbelin	2008-07-15
*	Correction d'un autre bug autour de la gestion des niveaux vides de	herbelin	2008-07-11
*	Bug résiduel du backtrack de coqide se produisant lorsque la limite de	herbelin	2008-07-10
*	- Improve [Context] vernacular to allow arbitrary binders, not just	msozeau	2008-07-07
*	Fixes in handling of implicit arguments:	msozeau	2008-07-04
*	Various bug fixes in type classes and subtac:	msozeau	2008-07-01
*	removed unwanted linebreaks in pretty printing	corbinea	2008-06-19