coq - The formal proof system

Age	Commit message (Expand)	Author
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
2003-10-04	Reparation plus juste de l'inefficacite avec loaded_modules (respecte l'ordre)	herbelin
2003-10-03	Correction bug explosion de la taille de la liste loaded_modules	herbelin
2003-03-12	* empty log message *	barras
2003-02-13	Chargement dynamique de .cma	delahaye
2002-08-02	Modules dans COQ\!\!\!\!	coq
2002-03-17	Meilleure gestion de la reduction dans Field	delahaye
2001-12-13	compat ocaml 3.03	filliatr
2001-11-05	Oops	barras
2001-11-05	GROS COMMIT:	barras
2001-10-17	Abstraction de l'immplementation de dirpath et implementation dans l'autre se...	herbelin
2001-10-17	Amélioration mise en page Print ML Module et Print ML Module	herbelin
2001-09-20	On ignore les répertoires qui ne correspondent pas à des idents	herbelin
2001-09-19	Protection hd d'une liste vide	herbelin
2001-08-10	Parsing	herbelin
2001-05-23	amelioration des messages d'erreurs vis a vis des evars	barras
2001-04-03	utilisation de Options.if_verbose	filliatr
2001-03-15	entetes	filliatr
2001-02-07	Centralisation des add_path dans Mltop a cause de la dependance en add_ml_dir	herbelin
2000-11-29	load_path_entry structure simplified; field relative_subdir renamed to coq_di...	sacerdot
2000-11-29	Ajout d'un alias à add_path, rec_add_path et all_subdirs pour associer un ch...	herbelin