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-12-02	Changement des named_context	gregoire
2005-04-20	Implementation of a new backtracking system, that allow to go back	coq
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
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-06-14	Commentaires	herbelin
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-11-05	GROS COMMIT:	barras
2001-09-20	Transparent	barras
2001-03-15	entetes	filliatr
2001-02-08	exporting traverse_to and mutate: they are used in pcoq.	bertot
2000-12-12	syntaxe AST Inversion + commentaires ocamlweb autour de $	filliatr
2000-11-02	correction Abstract (et make world passe!)	filliatr
2000-10-18	Renommage canonique :	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-23	Doc	herbelin
2000-05-18	doc	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
1999-12-10	- erreurs Pretype	filliatr
1999-12-10	debug reset	filliatr
1999-12-05	premier debugage	filliatr
1999-12-03	modules profile, Coqinit et Coqtop (=main)	filliatr
1999-12-01	poursuite de Vernacentries	filliatr
1999-12-01	module Pfedit	filliatr
1999-10-19	module Refiner	filliatr
1999-10-18	- déplacement (encore une fois !) des variables existentielles : elles sont	filliatr
1999-09-28	quelques trucs necessaires au toplevel	filliatr