coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	More monomorphic List.mem + List.assoc + ...	letouzey	2013-10-24
*	Delayed the computation of parameters in sort polymorphism of	herbelin	2013-05-14
*	Splitting Term into five unrelated interfaces:	ppedrot	2013-04-29
*	A more informative message when the elimination predicate for	herbelin	2013-02-17
*	Moved code from Pretype_error to Evarutil	ppedrot	2013-02-10
*	Uniformization of the "anomaly" command.	ppedrot	2013-01-28
*	Taking into account the possibility of having a type of type which is	herbelin	2012-12-18
*	Monomorphization (pretyping)	ppedrot	2012-11-22
*	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot	2012-09-14
*	This patch removes unused "open" (automatically generated from	regisgia	2012-09-14
*	The new ocaml compiler (4.00) has a lot of very cool warnings,	regisgia	2012-09-14
*	Updating headers.	herbelin	2012-08-08
*	Noise for nothing	pboutill	2012-03-02
*	Renamig support added to "Arguments"	gareuselesinge	2011-11-21
*	Still more unification in typing.ml	herbelin	2011-10-25
*	More unification in type_of and addition of e_type_of to get the new	herbelin	2011-10-24
*	Unification in the return clause of match was not supported in solve_evars.	herbelin	2011-10-11
*	Applied the trick of Chung-Kil Hur to solve second-order matching	herbelin	2011-10-10
*	It happens that the type inference algorithm (pretyping) did not check	herbelin	2011-10-05
*	Replaced printing number of ill-typed branch by printing name of constructor	herbelin	2011-04-08
*	Some dead code removal, thanks to Oug analyzer	letouzey	2010-09-24
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Added a function in typing.ml to solve evars of a constr w/o going back down ...	herbelin	2010-04-05
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Jolification : tentative de supprimer les "( evd)" et associés qui	aspiwack	2009-07-07
*	On remplace evar_map par evar_defs (seul evar_defs est désormais exporté	aspiwack	2009-02-19
*	Bugs, nettoyage, et améliorations diverses	herbelin	2008-04-13
*	Application de refresh_universes dans typing.ml et retyping.ml : les	herbelin	2008-03-15
*	Suppression des type_app et body_of_type qui alourdissent inutilement le code	herbelin	2007-08-27
*	Unification des types + clause filtrage manquante + uniformisation locale	herbelin	2007-06-07
*	Correction pour le rapport de bug #1325 par rétablissement du	herbelin	2007-01-22
*	Extension du polymorphisme de sorte au cas des définitions dans Type.	herbelin	2006-10-28
*	- Indtypes: en attente opinion CoRN, les occurrences de Type non explicites	herbelin	2006-05-28
*	Nouvelle implantation du polymorphisme de sorte pour les familles inductives	herbelin	2006-05-23
*	Inductifs avec polymorphisme de sorte (version initiale)	herbelin	2006-03-29
*	Changement des named_context	gregoire	2005-12-02
*	essai de typage des instantiations d\'evars	barras	2005-06-06
*	Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changed	sacerdot	2005-01-14
*	restructuration des printers: proofs passe avant parsing	barras	2004-09-17
*	hiding the meta_map in evar_defs	barras	2004-09-15
*	premiere reorganisation de l\'unification	barras	2004-09-03
*	Nouvelle en-tête	herbelin	2004-07-16
*	test de conversion laissait echapper exception NotConvertible	barras	2004-05-14
*	Commentaires	herbelin	2002-12-10
*	Essai suppression nf_betaiota dans type_of	herbelin	2002-12-09
*	petite erreur dans le typage des let-in	barras	2002-03-28
*	typage du produit: type_judgment appele avec contexte incorrect	barras	2002-02-19
*	Suites modifs du noyau. Univ devient purement fonctionnel.	barras	2001-11-12