coq - The formal proof system

Age	Commit message (Expand)	Author
2014-07-03	Fix eta expansion of primitive records (HoTT bug #78), which now fails cleanl...	Matthieu Sozeau
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2014-03-05	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey
2013-10-31	Conv_orable made functional and part of pre_env	gareuselesinge
2012-12-18	Modulification of name	ppedrot
2012-12-14	Modulification of identifier	ppedrot
2012-11-28	Kernel/closure: add eta red_kind	pboutill
2012-08-08	Updating headers.	herbelin
2011-02-17	- Use transparency information all the way through unification and	msozeau
2010-09-24	Some dead code removal, thanks to Oug analyzer	letouzey
2010-09-20	Added eta-expansion in kernel, type inference and tactic unification,	herbelin
2010-07-24	Updated all headers for 8.3 and trunk	herbelin
2010-06-22	New script dev/tools/change-header to automatically update Coq files headers.	herbelin
2010-04-29	Various minor improvements of comments in mli for ocamldoc	letouzey
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2010-04-29	Move from ocamlweb to ocamdoc to generate mli documentation	pboutill
2009-10-21	This big commit addresses two problems:	soubiran
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-02-06	pushed evar reduction in kernel	barras
2008-03-10	fold travaille maintenant sur la forme beta-iota-zeta réduite du	herbelin
2007-06-21	Correction de plusieurs bugs de l'export XML (utilisation d'un type de	herbelin
2006-10-05	Correction de deux cas où les types inductifs n'étaient pas comparés	herbelin
2006-05-05	amelioration de la machine interpretee (vecteurs au lieu de listes d'arguments)	barras
2005-12-02	Changement des named_context	gregoire
2005-11-18	petites corrections + contournement bug projections	barras
2005-07-13	* empty log message *	barras
2005-07-12	test du tag de reduction	barras
2004-10-20	COMMITED BYTECODE COMPILER	barras
2004-07-16	Nouvelle en-tête	herbelin
2003-08-06	Ajout de l'opti des fermeture (mais debranche pour l'instant)	barras
2003-08-05	Improved reduction machine with closure: should use less memory	barras
2002-11-14	Réforme de l'interprétation des termes :	herbelin
2002-08-16	Strengthenning rules for modules + No modules in sections	coq
2002-08-02	Modules dans COQ\!\!\!\!	coq
2002-01-30	cosmetique	herbelin
2001-11-29	nouvel algo de conversion plus uniforme	barras
2001-11-09	MAJ pour make doc	herbelin
2001-11-05	GROS COMMIT:	barras
2001-10-09	Suppression des arguments sur les constantes, inductifs et constructeurs	barras
2001-09-20	Transparent	barras
2001-09-20	Nettoyage des commentaires	herbelin
2001-09-05	Version de la reduction dans Closure plus econome en memoire:	barras
2001-07-02	Nettoyage/restructuration des ensembles d'indicateurs de réductions	herbelin
2001-05-28	option -quality	filliatr
2001-05-03	Changement de la structure des points fixes	barras
2001-04-15	to_constr renvoie directement un constr pour contourner l'ancien Term.mk_cons...	herbelin
2001-03-23	amelioration de la consommation memoire de la conversion en eta-expansant	barras
2001-03-15	entetes	filliatr
2001-03-01	nouvelle implantation de la reduction	barras
2001-01-31	Mise en place de la possibilite d'unfolder des variables locales et des const...	filliatr