coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	An automatic substitution of scope at functor application	letouzey	2011-02-11
*	Annotations at functor applications:	letouzey	2011-02-11
*	More {raw => glob} changes for consistency	glondu	2010-12-24
*	Rename rawterm.ml into glob_term.ml	glondu	2010-12-23
*	Change of nomenclature: rawconstr -> glob_constr	glondu	2010-12-23
*	Partial review of removed dead code (r13460)	herbelin	2010-09-24
*	Some dead code removal, thanks to Oug analyzer	letouzey	2010-09-24
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Extension of the recursive notations mechanism	herbelin	2010-07-22
*	Fixed wrong spelling in a warning.	herbelin	2010-06-08
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Optimized need for delimiters when disjoint scopes for strings and	herbelin	2010-04-10
*	Several bug-fixes and improvements of coqdoc	herbelin	2010-03-29
*	list, length, app are migrated from List to Datatypes	letouzey	2009-11-02
*	Local/Global revision 12418 continued	herbelin	2009-10-26
*	New cleaning phase of the Local/Global option management	herbelin	2009-10-26
*	Improved the treatment of Local/Global options (noneffective Local on	herbelin	2009-10-25
*	This big commit addresses two problems:	soubiran	2009-10-21
*	Remove useless Liboject.export_function field	glondu	2009-09-17
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Generalized the possibility to refer to a global name by a notation	herbelin	2009-09-11
*	Death of "survive_module" and "survive_section" (the first one was	herbelin	2009-08-13
*	- Cleaning phase of the interfaces of libnames.ml and nametab.ml	herbelin	2009-08-06
*	Fix a small notation/scope bug:	vsiles	2009-04-30
*	pushed evar reduction in kernel	barras	2009-02-06
*	Affichage des notations récursives:	herbelin	2008-10-22
*	Backporting 11445 from 8.2 to trunk (negative conditions in	herbelin	2008-10-11
*	Correct implementation of discharging of implicit arguments and add new	msozeau	2008-07-22
*	Uniformisation du format des messages d'erreur (commencent par une	herbelin	2008-07-17
*	Documentation Prop<=Set et Arguments Scope Global	herbelin	2008-07-01
*	Mises à jour test-suite + amélioration message d'erreur pour non-bug #1757	herbelin	2008-05-07
*	Add the ability to specify the implicit status of section variables and	msozeau	2008-04-02
*	Plus de combinateurs sont passés de Util à Option. Le module Options	aspiwack	2007-12-06
*	Factorisation des opérations sur le type option de Util dans un module	aspiwack	2007-12-05
*	Prise en compte réversibilité des notations de la forme "Notation Nil := @n...	herbelin	2007-05-10
*	Ajout de la possibilité de faire référence dans certains cas à un nom	herbelin	2007-04-28
*	Une passe sur les warnings (ajout Options.warn déclenchée par compile-verbo...	herbelin	2007-02-24
*	Suite commit restructuration discharge (application du type de	herbelin	2007-01-10
*	Nouvelle approche pour le discharge modulaire	herbelin	2007-01-10
*	Add a flush for a warning.	courtieu	2006-10-23
*	Annulation de l'essai de changement de sémantique du %scope (révision 9208).	herbelin	2006-10-06
*	Essai de changement de sémantique du %scope :	herbelin	2006-10-05
*	Correction bug #1179 (result of Notation.decompose_notation_key in wrong order	herbelin	2006-09-23
*	Standardisation nom option_app en option_map	herbelin	2006-04-27
*	Utilisation du section_path pour le parsing des notations primitives,	herbelin	2006-02-04
*	Adaptation message d'erreur au cas des string	herbelin	2006-01-31
*	Suppression de la dépendance en Map.fold de ocaml dont la sémantique a	herbelin	2006-01-24
*	Automatisation de l'utilisation de token primitifs dans les motifs de filtrag...	herbelin	2006-01-08
*	Ajout d'un mécanisme d'interprétation et d'affichage pour les littéraux de...	herbelin	2005-12-30
*	Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...	herbelin	2005-12-26