coq - The formal proof system

Age	Commit message (Expand)	Author
2017-02-15	[stm] Break stm/toplevel dependency loop.	Emilio Jesus Gallego Arias
2016-08-19	Make the user_err header an optional parameter.	Emilio Jesus Gallego Arias
2016-08-19	Remove errorlabstrm in favor of user_err	Emilio Jesus Gallego Arias
2016-07-03	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey
2016-06-29	A new infrastructure for warnings.	Maxime Dénès
2016-05-31	Feedback cleanup	Emilio Jesus Gallego Arias
2016-01-20	Update copyright headers.	Maxime Dénès
2015-02-19	Adding a possible DEPRECATED flag to VERNAC EXTEND statements.	Pierre-Marie Pédrot
2015-01-12	Update headers.	Maxime Dénès
2014-12-16	Getting rid of Exninfo hacks.	Pierre-Marie Pédrot
2014-09-10	VernacExtend does not dispatch on type anymore.	Pierre-Marie Pédrot
2013-06-06	More comments in Genarg.	ppedrot
2013-04-15	More functional implementation of locality_flag and program_mode	gareuselesinge
2013-03-13	Vernac+Toplevel: get rid of Error_in_file	letouzey
2013-03-13	Restrict (try...with...) to avoid catching critical exn (part 13)	letouzey
2013-01-28	Actually adding backtrace handling.	ppedrot
2012-10-02	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey
2012-09-14	Partial revert of Yann commit in order to use CLib.List when opening	ppedrot
2012-09-14	This patch removes unused "open" (automatically generated from	regisgia
2012-08-08	Updating headers.	herbelin
2012-06-01	Getting rid of Pp.msgnl and Pp.message.	ppedrot
2012-05-29	Vernacexpr is now a mli-only file, locality stuff now in locality.ml	letouzey
2012-03-02	Noise for nothing	pboutill
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-04-29	Remove the svn-specific $Id$ annotations	letouzey
2009-12-08	Migration of ProtectedToplevel and Line_oriented_parser into new contrib Inte...	letouzey
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2008-07-17	Uniformisation du format des messages d'erreur (commencent par une	herbelin
2007-12-06	Plus de combinateurs sont passés de Util à Option. Le module Options	aspiwack
2005-12-26	Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...	herbelin
2004-07-16	Nouvelle en-tête	herbelin
2002-08-02	Modules dans COQ\!\!\!\!	coq
2002-05-29	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin
2001-12-13	compat ocaml 3.03	filliatr
2001-09-20	Transparent	barras
2001-09-07	Suppression des library roots, on teste si un nom est absolu autrement	herbelin
2001-08-10	Parsing	herbelin
2001-03-15	entetes	filliatr
2001-03-01	Déplacement de qualid dans Nametab, hors du noyau	herbelin
2000-11-22	Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's...	herbelin
2000-11-20	Prise en compte des noms qualifiés dans certaines commandes	herbelin
2000-10-30	Ajout d'un switch pour le debugger	delahaye
2000-06-02	Bugs/Messages d'erreurs	herbelin
2000-05-04	Nettoyage de l'interface de Pfedit	herbelin
2000-05-03	Ajout du langage de tactiques	delahaye
2000-01-07	Renommage command en constr	herbelin
1999-12-03	modules profile, Coqinit et Coqtop (=main)	filliatr
1999-11-24	Vernacinterp et Vernacentries (partiellement)	filliatr