coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Move Record desugaring to constrintern and add ability to use notations	msozeau	2008-11-05
*	Petit bug dans le commit précédent.	aspiwack	2008-11-05
*	Nouvelle syntaxe pour écrire des records (co)inductifs :	aspiwack	2008-11-05
*	Remove calls to Dynlink.add_{interfaces,available_units} altogether	glondu	2008-10-29
*	Native "Declare ML Module" when possible	glondu	2008-10-28
*	11511 continued (bug in set.out + incohérence dans "Theorem with"	herbelin	2008-10-28
*	- Fixed many "Theorem with" bugs.	herbelin	2008-10-27
*	Fixes and refinements regarding occurrence selection:	herbelin	2008-10-26
*	- MAJ svn:ignore pour bin/coq-parser (anciennement bin/parser)	herbelin	2008-10-26
*	Raise informative errors instead of Failures or anomalies in case a meta	msozeau	2008-10-24
*	Open notation for declaring record instances.	msozeau	2008-10-23
*	Generalized implementation of generalization.	msozeau	2008-10-23
*	Fix bugs #1975 and #1976.	msozeau	2008-10-22
*	Affichage des notations récursives:	herbelin	2008-10-22
*	- Export de pattern_ident vers les ARGUMENT EXTEND and co.	herbelin	2008-10-19
*	Backporting 11445 from 8.2 to trunk (negative conditions in	herbelin	2008-10-11
*	Fix bug #1959 (remember: never use a partial functions mindlessly).	msozeau	2008-10-08
*	Minor fixes related to coqdoc and --interpolate and the dependent	msozeau	2008-10-03
*	Fix bug #1943 and restrict the inference optimisation of Program to	msozeau	2008-09-15
*	Add user syntax for creating hint databases [Create HintDb foo	msozeau	2008-09-14
*	In manual implicit arguments mode, do not enrich implicits	msozeau	2008-09-14
*	Fix bug #1936: uncaught exception due to undefinable exceptions.	msozeau	2008-09-14
*	Fix bug #1940: uncaught exception when searching for a type class.	msozeau	2008-09-14
*	Add enough information to correctly globalize recursive calls in inductive and	msozeau	2008-09-11
*	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
*	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
*	Various fixes w.r.t typeclasses and subtac: resolve tcs properly inside	msozeau	2008-08-21
*	eviter redondance du message d'erreur (Error while reading / File)	barras	2008-08-07
*	Correction de bugs:	herbelin	2008-08-05
*	Report des commits 11297 et 11299 (nom Unnamed_theorem local caché par	herbelin	2008-08-04
*	Évolutions diverses et variées.	herbelin	2008-08-04
*	Fixes in generalize_eqs/dependent induction to allow the user to specify	msozeau	2008-07-28
*	- Pour CoRN, rétablissement notations Qgt/Qge (mais cette fois avec	herbelin	2008-07-26
*	Fixed bug #1904 (instances of evars were no longer substituted since	herbelin	2008-07-25
*	Fix bug #1913, checking for unresolved evars which aren't obligations.	msozeau	2008-07-24
*	Suite commit 11236	notin	2008-07-24
*	Stop glob messages to be printed by default on stdout	letouzey	2008-07-23
*	Correct implementation of discharging of implicit arguments and add new	msozeau	2008-07-22
*	Suite commit 11236	notin	2008-07-21
*	Rétablissement de l'option -dump-glob de coq top et de l'option -glob-from d...	notin	2008-07-18
*	Affichage intempestif d'information de globalisation + numéro de version dan...	notin	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
*	Suite de la révision #11212	notin	2008-07-08
*	Fix implicit arguments in sections bug and check for resolution of evars when	msozeau	2008-07-07
*	Utilisation de try_locate_qualified_library au lieu de locate_qualified_libra...	notin	2008-07-07
*	- Improve [Context] vernacular to allow arbitrary binders, not just	msozeau	2008-07-07