coq - The formal proof system

Age	Commit message (Expand)	Author
2012-10-06	Turn mltop.ml4 into a regular ocaml file	letouzey
2012-10-02	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey
2012-09-17	More cleaning on Utils and CList. Some parts of the code being	ppedrot
2012-08-08	Updating headers.	herbelin
2012-07-12	Ensure that a plugin init function is called only once	letouzey
2012-06-01	Cleaning Pp.ppnl use	ppedrot
2012-06-01	Getting rid of Pp.msgnl and Pp.message.	ppedrot
2012-05-30	Getting rid of Pp.msg	ppedrot
2012-05-30	More uniformisation in Pp.warn functions.	ppedrot
2012-04-12	lib directory is cut in 2 cma.	pboutill
2012-03-02	Noise for nothing	pboutill
2012-01-26	Add support for plugin initialization function	gareuselesinge
2011-12-17	A pass on warning printings. Made systematic the use of msg_warning so	herbelin
2011-11-02	Add type annotations around all calls to Libobject.declare_object	letouzey
2010-10-31	Minor code improvements around libobject	herbelin
2010-09-28	Fix function applications without labels (OCaml warning 6)	glondu
2010-09-24	Some dead code removal, thanks to Oug analyzer	letouzey
2010-07-24	Updated all headers for 8.3 and trunk	herbelin
2010-05-19	static (and shared) camlp4use instead of per-file declaration	letouzey
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2009-10-21	This big commit addresses two problems:	soubiran
2009-09-29	Add support for Local Declare ML Module	glondu
2009-09-17	Replace unprotected call to where_in_path by find_file_in_path	glondu
2009-09-17	Remove useless Liboject.export_function field	glondu
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-08-13	Death of "survive_module" and "survive_section" (the first one was	herbelin
2009-08-06	- Cleaning phase of the interfaces of libnames.ml and nametab.ml	herbelin
2009-03-17	- configure: affiche si le natdynlink est positionne	barras
2009-03-14	Better mechanism for loading initial plugins	letouzey
2009-02-03	Allow to turn contrib/subtac into a (nat)dynlink'able plugin	letouzey
2009-01-18	Backporting from v8.2 to trunk:	herbelin
2009-01-05	Completed 11745 (move of jprover to user contribs) and cleaned 11743	herbelin
2008-12-24	- coq_makefile: target install now respects the original tree structure	herbelin
2008-12-17	Sequel of 11697: repair coqtop.byte when contribs are statically linked (+min...	letouzey
2008-12-16	Take advantage of natdynlink when available: almost all contribs become loada...	letouzey
2008-11-23	- Synchronized subst_object with load_object (load_and_subst_objects)	herbelin
2008-11-22	- Fixed minor bug #1994 in the tactic chapter of the manual [doc]	herbelin
2008-10-29	Remove calls to Dynlink.add_{interfaces,available_units} altogether	glondu
2008-10-28	Native "Declare ML Module" when possible	glondu
2008-07-17	Uniformisation du format des messages d'erreur (commencent par une	herbelin
2008-06-29	Lissage de la gestion des chemins de chargement de fichiers :	herbelin
2007-12-06	Plus de combinateurs sont passés de Util à Option. Le module Options	aspiwack
2007-09-15	* Adding compability with ocaml 3.10 + camlp5 (rework of	letouzey
2007-07-13	New bootstrapping, improved, Makefile system	corbinea
2006-11-21	Nettoyage de l'utilisation de l'expansion des macros ~ et $ dans les noms de	herbelin
2005-02-06	Nettoyage et documentation de Library	herbelin
2004-07-17	Backtrack sur l'utilisation de pa_macro car n'existait pas en 3.06	herbelin
2004-07-16	Branchement sur pa_macro, pa_ifdef devenant obsolete en 3.08	herbelin
2004-07-16	Nouvelle en-tête	herbelin
2003-10-07	Correction du bug 335 et Export/Require Export dans un module	coq