coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd	letouzey	2012-05-29
*	Pfedit: two superfluous open	letouzey	2012-05-29
*	Remove old proof-managment commands Suspend/Resume	letouzey	2012-03-23
*	Pfedit: avoid Undoing too much	letouzey	2012-03-21
*	Noise for nothing	pboutill	2012-03-02
*	Proof using ...	gareuselesinge	2011-12-12
*	Fixing Implicit Tactic mode damaged by commit r14496 (see also bug #2612).	herbelin	2011-10-05
*	Moving implicit tactic support from Tacinterp to Pfedit and final evar	herbelin	2011-09-26
*	The modules in proofs now use the Errors module to explain their exceptions t...	aspiwack	2011-05-13
*	Revert "Add [Polymorphic] flag for defs"	msozeau	2011-04-13
*	Add [Polymorphic] flag for defs	msozeau	2011-04-13
*	Applying Tom Prince's patch for build_constant_by_tactic not able to	herbelin	2011-04-08
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Fix: Pfedit.get_current_goal_context when no goal is focused.	aspiwack	2010-05-10
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Here comes the commit, announced long ago, of the new tactic engine.	aspiwack	2010-04-22
*	Added support for definition of fixpoints using tactics.	herbelin	2009-11-27
*	A bit of cleaning around name generation + creation of dedicated file namegen.ml	herbelin	2009-11-09
*	Restructuration of command.ml + generic infrastructure for inductive schemes	herbelin	2009-11-08
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Fixed bugs #2001 (search_guard was overwriting the guard index given	herbelin	2009-01-04
*	Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuve	herbelin	2008-04-25
*	Merge with lmamane's private branch:	lmamane	2008-02-22
*	Declarative Proof Language: main commit	corbinea	2006-09-20
*	Implementation of a new backtracking system, that allow to go back	coq	2005-04-20
*	Suppression de la dépendance en Tacmach pour pouvoir être appelé de top_pr...	herbelin	2004-12-31
*	Code mort	herbelin	2004-11-18
*	COMMITED BYTECODE COMPILER	barras	2004-10-20
*	restructuration des printers: proofs passe avant parsing	barras	2004-09-17
*	Nouvelle en-tête	herbelin	2004-07-16
*	Export du type de preuve en cours pour xml	herbelin	2004-03-29
*	Gestion en temps constant de la pile des Unfo; affichage des buts par Pfedit ...	herbelin	2003-10-10
*	Mise en place d'un couple 'Conjecture/Admitted' pour déclarer un énoncé in...	herbelin	2003-10-08
*	open superflu	herbelin	2003-09-12
*	Pour satisfaire ProofGeneral	coq	2003-01-31
*	Ajout du vernac Proof with	gregoire	2002-12-12
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
*	simplification common_ancestor	courant	2002-11-13
*	Intégration des modifs de la branche mowgli :	herbelin	2002-11-05
*	Modules dans COQ\!\!\!\!	coq	2002-08-02
*	Ajout d'un point d'entree pour exporter les arbres de preuves en XML	herbelin	2002-07-24
*	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin	2002-05-29
*	changement de l'undo limit	barras	2002-04-03
*	compat ocaml 3.03	filliatr	2001-12-13
*	nouvel algo de conversion plus uniforme	barras	2001-11-29
*	Diverses petites simplications de la machine de preuves.	clrenard	2001-11-19
*	Suppression des local_constraints, des ctxtty et du focus.	clrenard	2001-11-06
*	GROS COMMIT:	barras	2001-11-05
*	Transparent	barras	2001-09-20
*	amelioration de la structure des univers	barras	2001-03-28