coq - The formal proof system

Age	Commit message (Expand)	Author
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
2000-11-02	correction Abstract (et make world passe!)	filliatr
2000-11-02	suppression des (* open Generic *)	filliatr
2000-09-10	Correction pour make doc	herbelin
2000-09-10	Ajout d'un LetIn primitif.	herbelin
2000-07-24	Passage à des contextes de vars et de rels pouvant contenir des déclarations	herbelin
2000-05-25	Déplacement de save_thm and co de PFedit vers Command	herbelin
2000-05-22	Suite restructuration inductifs; changement nom module Constant en Declarations	herbelin
2000-05-05	Achèvement nettoyage Pfedit	herbelin
2000-05-04	Nettoyage de l'interface de Pfedit	herbelin
2000-05-03	Ajout du langage de tactiques	delahaye