coq - The formal proof system

Age	Commit message (Expand)	Author
2013-04-29	Merging Context and Sign.	ppedrot
2013-04-29	Splitting Term into five unrelated interfaces:	ppedrot
2012-12-14	Modulification of identifier	ppedrot
2012-11-13	More monomorphizations	ppedrot
2012-09-14	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-08-08	Updating headers.	herbelin
2012-03-02	Noise for nothing	pboutill
2011-07-29	Environ: generic equality on named_context replaced by named_context_equal	puech
2010-07-24	Updated all headers for 8.3 and trunk	herbelin
2010-05-09	Added a few informations about file lineages (for the most part in kernel)	herbelin
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2008-12-31	Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->	herbelin
2008-01-18	bug in accessing n-th abstraction	barras
2007-12-05	Factorisation des opérations sur le type option de Util dans un module	aspiwack
2007-08-27	Suppression des type_app et body_of_type qui alourdissent inutilement le code	herbelin
2006-09-01	Ajout iter_rel_context/iter_named_context	herbelin
2006-05-23	Nouvelle implantation du polymorphisme de sorte pour les familles inductives	herbelin
2006-04-27	Standardisation nom option_app en option_map	herbelin
2005-12-02	Changement des named_context	gregoire
2005-02-18	Added map_named_context	herbelin
2004-10-20	COMMITED BYTECODE COMPILER	barras
2004-07-16	Nouvelle en-tête	herbelin
2003-12-16	bug #266 (Search Error si on calcule apres avoir fait Clear d'une var Local)	barras
2002-08-02	Modules dans COQ\!\!\!\!	coq
2002-04-04	resolution du pb d'efficacite du a Sign.add_named_decl	barras
2002-03-22	code redondant	herbelin
2002-02-22	suppression de pop_named	barras
2002-02-14	- Reforme de la gestion des args recursifs (via arbres reguliers)	barras
2001-12-13	compat ocaml 3.03	filliatr
2001-11-20	Ajout mkArity	herbelin
2001-11-20	types vs constr	herbelin
2001-11-12	Suites modifs du noyau. Univ devient purement fonctionnel.	barras
2001-11-05	GROS COMMIT:	barras
2001-10-11	Suppression option immediate_discharge; nettoyage de Declare et conséquences	herbelin
2001-10-09	Suppression des arguments sur les constantes, inductifs et constructeurs	barras
2001-10-03	Correction messages d'erreur	herbelin
2001-09-14	exceptions	barras
2001-09-14	mauvais rattrapage d'exception	barras
2001-03-15	entetes	filliatr
2001-02-14	Mise en place d'un système optionnel de discharge immédiat; prise en compte...	herbelin
2000-11-27	Prise en compte des let in dans les instances de globaux	herbelin
2000-11-02	suppression des (* open Generic *)	filliatr
2000-10-18	Simplifications autour de typed_type (renommé types par analogie avec sorts)...	herbelin
2000-10-18	Renommage canonique :	herbelin
2000-10-03	Rebranchement de la tactique Let	herbelin
2000-09-10	Correction pour make doc	herbelin
2000-09-10	Ajout d'un LetIn primitif.	herbelin
2000-07-24	Passage à des contextes de vars et de rels pouvant contenir des déclarations	herbelin
2000-05-22	Renommage hypothèses de nom redondant dans les environnements	herbelin