coq - The formal proof system

Age	Commit message (Expand)	Author
2012-11-22	Monomorphization (kernel)	ppedrot
2012-11-13	More monomorphizations	ppedrot
2012-10-29	Removed many calls to OCaml generic equality. This was done by	ppedrot
2012-08-08	Updating headers.	herbelin
2012-03-02	Noise for nothing	pboutill
2011-10-11	Names : check of labels, cleanup, nicer debug display of kn and constant	letouzey
2011-10-02	Hash-consing of constr could share more	letouzey
2011-09-22	Hash-consing: attempt to stop hash-consing separately constr in declare.ml	letouzey
2011-09-15	Names.make_mbid and co : convert from/to identifier (avoid some String.copy)	letouzey
2011-09-08	More twicks on hash-consing	letouzey
2011-05-11	Print Module (Type) M now tries to print more details	letouzey
2011-03-05	Moving printing of module typing errors upwards to himsg.ml so as to	herbelin
2011-02-11	compatibility <3.12 (Map.exists Map.singleton)	pboutill
2011-01-27	Make simpl use the proper constant when folding (mutual) fixpoints	letouzey
2010-07-24	Updated all headers for 8.3 and trunk	herbelin
2010-06-23	Names: remove obsolete mod_self_id	letouzey
2010-06-22	New script dev/tools/change-header to automatically update Coq files headers.	herbelin
2010-04-29	After the approval of Bruno, here the patch for the checker.	soubiran
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
2010-04-16	Names.mli: double declaration of mind_modpath	letouzey
2009-10-21	This big commit addresses two problems:	soubiran
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2008-10-15	Report des commits 11417 et 11437 de la v8.2	soubiran
2008-06-25	Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisatio...	notin
2008-05-11	- Cleanup parsing of binders, reducing to a single production for all	msozeau
2008-04-21	- Parameterize unification by two sets of transparent_state, one for open	msozeau
2007-12-18	Nettoyage de code en vue de la release. Plus de Warning: Unused	aspiwack
2007-05-11	Processor integers + Print assumption (see coqdev mailing list for the	aspiwack
2007-02-21	Fixed the pseudo-cicularity problem due to the with operator on Module Type.	soubiran
2007-01-24	modifications des messages d'erreurs renvoyés lors de la comparaison	soubiran
2006-05-23	Modification de add_glob (support des modules dans Coqdoc)	notin
2005-02-18	Moved Indmap and ConstrMap from Libnames to Names for use in Cooking	herbelin
2004-11-16	Names.substitution (and related functions) and Term.subst_mps moved to	sacerdot
2004-11-16	IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).	sacerdot
2004-10-20	COMMITED BYTECODE COMPILER	barras
2004-07-16	Nouvelle en-tête	herbelin
2003-01-22	id_of_msid en plus	letouzey
2002-12-09	Corrections de gestion des univers et modules + meilleure gestions des noms...	coq
2002-12-05	des Set et des Map en plus	letouzey
2002-12-04	Corrige un bug de composition de substitutions	coq
2002-11-14	Réforme de l'interprétation des termes :	herbelin
2002-08-19	Pretty-printing preliminaire des modules, commandes	coq
2002-08-02	Modules dans COQ\!\!\!\!	coq
2001-11-29	reparation de Locate	barras
2001-11-29	nouvel algo de conversion plus uniforme	barras
2001-11-12	Suites modifs du noyau. Univ devient purement fonctionnel.	barras
2001-11-05	GROS COMMIT:	barras
2001-10-17	Abstraction de l'immplementation de dirpath et implementation dans l'autre se...	herbelin