coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Add type annotations around all calls to Libobject.declare_object	letouzey	2011-11-02
*	Clarifying that only identifiers are advertised to be turned into keywords	herbelin	2011-08-23
*	Partly revert commit r14389 about relaxing the condition for being a keyword	herbelin	2011-08-10
*	Be a bit less aggressive in declaring idents as keywords in notations	herbelin	2011-08-08
*	Fixed notation printing bug when curly brackets are involved (requests	herbelin	2011-04-28
*	Rename rawterm.ml into glob_term.ml	glondu	2010-12-23
*	About "unsupported" unicode characters in notations.	herbelin	2010-10-17
*	Backporting r13521 from branch 8.3 to trunk (fixing bug #2406, looping	herbelin	2010-10-11
*	Some dead code removal, thanks to Oug analyzer	letouzey	2010-09-24
*	Fix unescaped end-of-lines (OCaml warning 29)	glondu	2010-09-13
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Extension of the recursive notations mechanism	herbelin	2010-07-22
*	Fixing spelling: pr_coma -> pr_comma	herbelin	2010-06-12
*	Add (almost) compatibility with camlp4, without breaking support for camlp5	letouzey	2010-05-19
*	Nicer representation of tokens, more independant of camlp*	letouzey	2010-05-19
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Several bug-fixes and improvements of coqdoc	herbelin	2010-03-29
*	Added automatic expansion on the left of recursive notations	herbelin	2010-03-23
*	Fix for notation scope & inductive types	vsiles	2009-11-25
*	Improving abbreviations/notations + backtrack of semantic change in r12439	herbelin	2009-11-11
*	Restructuration of command.ml + generic infrastructure for inductive schemes	herbelin	2009-11-08
*	This big commit addresses two problems:	soubiran	2009-10-21
*	Remove legacy export_* functions	glondu	2009-09-29
*	Remove useless Liboject.export_function field	glondu	2009-09-17
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	- Addition of "Reserved Infix" continued.	herbelin	2009-09-14
*	Generalized the possibility to refer to a global name by a notation	herbelin	2009-09-11
*	Add support for "Infix ... := constr" instead of just "Infix ... := ref".	herbelin	2009-08-11
*	- Cleaning phase of the interfaces of libnames.ml and nametab.ml	herbelin	2009-08-06
*	- Fixed a little bug in previous commit (bad failure in case of unknown entry).	herbelin	2009-04-27
*	- Cleaning (unification of ML names, removal of obsolete code,	herbelin	2009-04-27
*	- Fixing #2090 (occur check missing when trying to solve evar-evar equation).	herbelin	2009-04-25
*	- Structuring Numbers and fixing Setoid in stdlib's doc.	herbelin	2009-01-19
*	Fixing #1960 (xml bug with external on goal variable) and #1961	herbelin	2009-01-14
*	- MAJ svn:ignore pour bin/coq-parser (anciennement bin/parser)	herbelin	2008-10-26
*	Affichage des notations récursives:	herbelin	2008-10-22
*	- Export de pattern_ident vers les ARGUMENT EXTEND and co.	herbelin	2008-10-19
*	Correction de bugs:	herbelin	2008-08-05
*	Uniformisation du format des messages d'erreur (commencent par une	herbelin	2008-07-17
*	Correction bug 1878 (utilisation de extend_evar déplacée là où une	herbelin	2008-06-14
*	Ajout d'abbréviations/notations paramétriques	herbelin	2008-03-30
*	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
*	* Adding compability with ocaml 3.10 + camlp5 (rework of	letouzey	2007-09-15
*	Prévention notations récursives sans terminal à gauche et qui font boucler	herbelin	2007-03-15
*	Suppression d'un résidu de la syntaxe v7 (Print Grammar avec univ)	herbelin	2007-02-24
*	gestion speciale du niveau 5 des ltac	barras	2006-11-02
*	Amélioration de l'automatisation des coupures quand deux idents se suivent	herbelin	2006-10-09
*	CompatibilitÃ© hyp=var dans Tactic Notation + nettoyage	herbelin	2006-09-15
*	Prise en compte de notations numérales définies au niveau utilisateur+ lég...	herbelin	2006-01-08