coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	STM: new "par:" goal selector, like "all:" but in parallel	Enrico Tassi	2014-08-05
*	Adding a stm/ folder, as asked during last workgroup. It was essentially moving	Pierre-Marie Pédrot	2014-04-25
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	State Transaction Machine	gareuselesinge	2013-08-08
*	raise UnsafeSuccess -> feedback AddedAxiom	gareuselesinge	2013-04-25
*	Updating headers.	herbelin	2012-08-08
*	Vecnacentries.dump_global silently ignores exceptions	pboutill	2012-08-06
*	A new status Unsafe in Interface. Meant for commands such as Admitted.	aspiwack	2012-07-12
*	Getting rid of Pcoq remains.	ppedrot	2012-06-12
*	New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr	letouzey	2012-05-29
*	locus.mli for occurrences+clauses, misctypes.mli for various little things	letouzey	2012-05-29
*	correct abort in Function when a proof of inversion fails	letouzey	2012-04-23
*	A unified backtrack mechanism, with a basic "Show Script" as side-effect	letouzey	2012-03-23
*	Noise for nothing	pboutill	2012-03-02
*	Adds a new command Show Goal (e.g. Show Goal "42") printing a goal using the...	aspiwack	2011-09-12
*	Coqide: new backtracking code, based on the Backtrack command	letouzey	2011-09-05
*	Misc improvements concerning "Show Match" and its coqide equivalent	letouzey	2011-08-18
*	New option [Set Bullet Behavior] allows to select the behaviour of bullets.	aspiwack	2011-05-13
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	New script dev/tools/change-header to automatically update Coq files headers.	herbelin	2010-06-22
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Move from ocamlweb to ocamdoc to generate mli documentation	pboutill	2010-04-29
*	Here comes the commit, announced long ago, of the new tactic engine.	aspiwack	2010-04-22
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Generalized the possibility to refer to a global name by a notation	herbelin	2009-09-11
*	Merge with lmamane's private branch:	lmamane	2008-02-22
*	Merge from Lionel Elie Mamane's private branch:	lmamane	2007-01-10
*	Cleanning and factorizing code in funind. Spliting new_arg_principles into to...	jforest	2006-05-03
*	Compatibilité ocamlweb pour cible doc	herbelin	2005-01-21
*	Nouvelle en-tête	herbelin	2004-07-16
*	Deplacement pr_subgoal and co vers Pfedit	herbelin	2003-10-13
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
*	Modules dans COQ\!\!\!\!	coq	2002-08-02
*	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin	2002-05-29
*	Suite de la suppression : enamed_declaration est remplace par evar_map.	clrenard	2001-11-06
*	Suppression option immediate_discharge; nettoyage de Declare et conséquences	herbelin	2001-10-11
*	entetes	filliatr	2001-03-15
*	Déplacement de qualid dans Nametab, hors du noyau	herbelin	2001-03-01
*	export a function that is needed in pcoq.	bertot	2001-02-13
*	exported several functions that are used in the graphical interface pcoq.	bertot	2001-02-09
*	export a function that can be used to retrieve the context corresponding	bertot	2001-02-08
*	syntaxe AST Inversion + commentaires ocamlweb autour de $	filliatr	2000-12-12
*	Uniformisation AddPath, Print LoadPath, ... en Add Path, Print Path. Abstract...	herbelin	2000-09-10
*	documentation interfaces	filliatr	1999-12-13
*	module Metasyntax	filliatr	1999-12-01
*	Vernacinterp et Vernacentries (partiellement)	filliatr	1999-11-24