coq - The formal proof system

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