coq - The formal proof system

Age	Commit message (Expand)	Author
2014-09-03	Fixing bug #2818.	Pierre-Marie Pédrot
2014-07-21	Unifying locate code, also making it more powerful: it is now able to find	Pierre-Marie Pédrot
2014-07-21	Adding a new "Locate Term" command, distinct from the raw "Locate" command.	Pierre-Marie Pédrot
2014-07-21	More complete printing of Ltac location, akin to the term-dedicated Locate co...	Pierre-Marie Pédrot
2014-04-23	Removing dead code, thanks to new OCaml warnings and a bit of scripting.	Pierre-Marie Pédrot
2013-03-13	Restrict (try...with...) to avoid catching critical exn (part 6)	letouzey
2013-02-19	Dir_path --> DirPath	letouzey
2012-12-14	Modulification of dir_path	ppedrot
2012-12-14	Modulification of identifier	ppedrot
2012-08-08	Updating headers.	herbelin
2012-06-22	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot
2012-05-29	remove many excessive open Util & Errors in mli's	letouzey
2012-05-29	global_reference migrated from Libnames to new Globnames, less deps in gramma...	letouzey
2012-03-02	Noise for nothing	pboutill
2010-07-24	Updated all headers for 8.3 and trunk	herbelin
2010-06-22	New script dev/tools/change-header to automatically update Coq files headers.	herbelin
2010-06-03	Added command "Locate Ltac qid".	herbelin
2010-04-29	"make source-doc" builds documentation of mli in html and pdf at	pboutill
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
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-09-11	Generalized the possibility to refer to a global name by a notation	herbelin
2009-08-07	Fixed incorrect optimization in Prettyp.pr_located_qualid introduced	herbelin
2009-08-06	Cleaning of Nametab continued + fixed a compilation bug in previous commit.	herbelin
2009-08-06	- Cleaning phase of the interfaces of libnames.ml and nametab.ml	herbelin
2009-01-01	Switched to "standardized" names for the properties of eq and	herbelin
2008-02-01	Beaoucoup de changements dans la representation interne des modules.	soubiran
2007-11-08	Prise en compte des notations "alias" dans la globalisation des coercions.	herbelin
2005-11-21	Correction bug dé-globalisation syntactic def (cf coq-club 20/11/05)	herbelin
2005-01-21	Compatibilité ocamlweb pour cible doc	herbelin
2004-07-16	Nouvelle en-tête	herbelin
2003-10-21	Nouvelle fonction cherchant tous les noms d'un suffixe donne	herbelin
2003-06-10	Passage des noms de tactiques à kernel_name pour compatibilité avec les fon...	herbelin
2003-04-07	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin
2003-03-12	* empty log message *	barras
2003-01-31	Pour satisfaire ProofGeneral	coq
2003-01-09	Export M + Module M <: SIG	coq
2002-11-26	Affichage nom le plus court pour Syntactic Definition	herbelin
2002-11-14	Réforme de l'interprétation des termes :	herbelin
2002-09-24	Un peu (plus) d'ordre dans Nametab...	coq
2002-09-24	Nametab data structure reorganisation	coq
2002-08-19	Pretty-printing preliminaire des modules, commandes	coq
2002-08-13	Petites corrections ici et la	coq
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-11-19	Re-installation de l'affichage des globaux par des noms courts	herbelin
2001-11-05	GROS COMMIT:	barras
2001-10-17	Abstraction de l'immplementation de dirpath et implementation dans l'autre se...	herbelin
2001-10-12	Déplacement de global_reference dans Names pour pouvoir lier Nametab à gra...	herbelin