coq - The formal proof system

Age	Commit message (Expand)	Author
2016-07-03	closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)	Pierre Letouzey
2016-07-01	Separate flags for fix/cofix/match reduction and clean reduction function names.	Maxime Dénès
2016-06-09	newring: fix for hack using evars as integers.	Matthieu Sozeau
2016-01-21	Merge branch 'v8.5'	Pierre-Marie Pédrot
2016-01-20	Update copyright headers.	Maxime Dénès
2015-09-14	Remove dead code in lazy reduction machine.	Maxime Dénès
2015-01-12	Update headers.	Maxime Dénès
2015-01-06	improve efficiency of the reduction interpreter of coqtop	Bruno Barras
2014-09-27	Add a boolean to indicate the unfolding state of a primitive projection,	Matthieu Sozeau
2014-09-13	Providing a -type-in-type option for collapsing the universe hierarchy.	Hugo Herbelin
2014-09-05	Rename eta_expand_ind_stacks, fix the one from the checker and adapt	Matthieu Sozeau
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