coq - The formal proof system

Age	Commit message (Expand)	Author
2003-11-01	Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les entie...	herbelin
2003-10-22	reorganisation des niveaux (ex: = est a 70)	barras
2003-10-16	Syntax error	herbelin
2003-10-16	Suppression des surcharge de regles de grammaire en v7	herbelin
2003-09-26	'Open Local Scope' en attendant que le core_scope sache se mettre devant impl...	herbelin
2003-09-26	Passage de Destruct a NewDestruct; '-' pour negb	herbelin
2003-06-13	FSets, mais pas compile' par make world	filliatr
2003-05-29	Ne pas mettre d'associatif a droite au niveau 3 en V7	herbelin
2003-05-21	Notations	herbelin
2003-04-29	Notations	herbelin
2002-07-09	Making the sumbool functions transparent, so that they can used to	bertot
2002-05-06	Standardisation	herbelin
2002-04-17	Uniformisation (Qed/Save et Implicits Arguments)	herbelin
2002-03-04	Nouveau Rewrite-in plus economique	barras
2002-02-28	Ajout andb_true_eq pour PolyList.list_beq	herbelin
2002-02-14	option -dump-glob pour coqdoc	filliatr
2001-09-27	Simplification de deux preuves. En outre ca simplifie leur extraction.	letouzey
2001-08-05	Expérimentation de NewDestruct et parfois NewInduction	herbelin
2001-04-19	Mise de (*i autour CVS info	mohring
2001-03-30	Ajout de lemmes sur les booleens	mohring
2001-03-15	entetes	filliatr
2001-02-01	- coqc : option -image	filliatr
2000-11-28	Elimination du '	delahaye
2000-11-05	Plus besoin de débrancher la preuve qui ne passait pas	herbelin
2000-05-03	Ajout du langage de tactiques	delahaye
2000-05-02	portage Omega (mais toujours pas Zpower et Zlogarithm)	filliatr
2000-03-16	mise sous CVS	filliatr