coq - The formal proof system

Age	Commit message (Expand)	Author
2011-09-12	Adds a new command Show Goal (e.g. Show Goal "42") printing a goal using the...	aspiwack
2011-09-05	Coqide: new backtracking code, based on the Backtrack command	letouzey
2011-08-18	Misc improvements concerning "Show Match" and its coqide equivalent	letouzey
2011-05-13	New option [Set Bullet Behavior] allows to select the behaviour of bullets.	aspiwack
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-04-29	Remove the svn-specific $Id$ annotations	letouzey
2010-04-29	Move from ocamlweb to ocamdoc to generate mli documentation	pboutill
2010-04-22	Here comes the commit, announced long ago, of the new tactic engine.	aspiwack
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
2008-02-22	Merge with lmamane's private branch:	lmamane
2007-01-10	Merge from Lionel Elie Mamane's private branch:	lmamane
2006-05-03	Cleanning and factorizing code in funind. Spliting new_arg_principles into to...	jforest
2005-01-21	Compatibilité ocamlweb pour cible doc	herbelin
2004-07-16	Nouvelle en-tête	herbelin
2003-10-13	Deplacement pr_subgoal and co vers Pfedit	herbelin
2002-11-14	Réforme de l'interprétation des termes :	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-11-06	Suite de la suppression : enamed_declaration est remplace par evar_map.	clrenard
2001-10-11	Suppression option immediate_discharge; nettoyage de Declare et conséquences	herbelin
2001-03-15	entetes	filliatr
2001-03-01	Déplacement de qualid dans Nametab, hors du noyau	herbelin
2001-02-13	export a function that is needed in pcoq.	bertot
2001-02-09	exported several functions that are used in the graphical interface pcoq.	bertot
2001-02-08	export a function that can be used to retrieve the context corresponding	bertot
2000-12-12	syntaxe AST Inversion + commentaires ocamlweb autour de $	filliatr
2000-09-10	Uniformisation AddPath, Print LoadPath, ... en Add Path, Print Path. Abstract...	herbelin
1999-12-13	documentation interfaces	filliatr
1999-12-01	module Metasyntax	filliatr
1999-11-24	Vernacinterp et Vernacentries (partiellement)	filliatr