coq - The formal proof system

Age	Commit message (Expand)	Author
2004-02-12	Décomposition automatique des règles d'analyse syntaxique pour les	herbelin
2003-11-29	Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...	herbelin
2003-10-28	Passage des notations de type dans type_scope	herbelin
2003-10-23	Commentaires	herbelin
2003-10-14	Argument de except, error implicite seulement en v8; Changement 'as notation'...	herbelin
2003-10-13	Argument implicite pour None, error, except	herbelin
2003-09-23	Fusion des fichiers de syntaxe de Init avec les fichiers de définition; Type...	herbelin
2003-05-21	Concentration des notations officielles dans Init/Notations; restructuration ...	herbelin
2003-04-09	Activation des implicites pour la v8	herbelin
2002-11-26	Bug ProjSn + retour de "Notation" pour déclarer les définitions syntaxiques	herbelin
2002-11-25	Retablissement SynDef Value/Error	herbelin
2002-11-24	Généralisation de l'utilisation de Notation	herbelin
2002-02-14	option -dump-glob pour coqdoc	filliatr
2002-01-31	changement generation de schema d'elimination, False_rec est primitif, Constr...	mohring
2002-01-09	MAJ des Id pour coqweb	herbelin
2001-11-14	Suppression d'Export redondants	herbelin
2001-09-27	and_rec redondant	letouzey
2001-08-30	Fin de la modif Exc/option	mohring
2001-08-29	ajout option , Exc --> option, et lemmes dans les theories	mohring
2001-08-05	Expérimentation de NewDestruct et parfois NewInduction	herbelin
2001-04-11	documentation automatique de la bibliothèque standard	filliatr
2001-03-30	Introduction d'une preuve de False_rec	mohring
2001-03-15	entetes	filliatr
1999-12-13	fichiers prelude Coq	filliatr