coq - The formal proof system

Age	Commit message (Expand)	Author
2003-11-02	Renommage bool en boolP pour eviter la qualification	herbelin
2003-11-02	Restauration preference Rge a Rle pour compatibilite...	herbelin
2003-11-02	Restauration preference Rge a Rle pour compatibilite...; petit nettoyage	herbelin
2003-11-01	Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les entie...	herbelin
2003-11-01	Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les entie...	herbelin
2003-10-30	Parsing du moins unaire au niveau de l'application qui n'a pas besoin d'etre ...	herbelin
2003-10-29	Choix sous sa forme relationnelle	herbelin
2003-10-28	Ordre (symbolique) des Require	herbelin
2003-10-28	Passage de la notations de paire dans core_scope	herbelin
2003-10-28	Passage des notations de type dans type_scope	herbelin
2003-10-28	Ajout %core; MAJ niveau connecteurs logique	herbelin
2003-10-28	MAJ	herbelin
2003-10-28	Fichier offrant l'axiome du choix unique en presence de logique classique	herbelin
2003-10-28	Fichier offrant l'axiome du choix en presence de logique classique	herbelin
2003-10-28	La logique sur Type inclut celle sur Set	herbelin
2003-10-28	Retour en arriere sur d'autres renommages de variables	herbelin
2003-10-27	Retour a un nommage non standard des variables pour compatibilite; report 're...	herbelin
2003-10-27	Bug du commit precedent	herbelin
2003-10-23	Commentaires	herbelin
2003-10-22	Documentation/Structuration	herbelin
2003-10-22	Documentation/Structuration	herbelin
2003-10-22	reorganisation des niveaux (ex: = est a 70)	barras
2003-10-21	Redondance de dec_eq_nat	herbelin
2003-10-21	Type relation dans Datatypes	herbelin
2003-10-21	Maintenant avant Datatypes	herbelin
2003-10-21	ajouts	herbelin
2003-10-20	R passe dans Set !	herbelin
2003-10-17	20 est uniquement associatif a gauche	herbelin
2003-10-17	Des implicites plus 'naturels' pour eq_ind, identity_ind and co	herbelin
2003-10-16	nouvelle syntaxe de ltac	barras
2003-10-16	lettac -> set	barras
2003-10-16	Syntax error	herbelin
2003-10-16	Suppression des surcharge de regles de grammaire en v7	herbelin
2003-10-16	Pour eviter des regles redondantes en v7	herbelin
2003-10-16	FTC_P2 maintenant dans RIneq	herbelin
2003-10-16	Ajout de quelques lemmes cles	herbelin
2003-10-15	Affichage = au lieu de == en v7	herbelin
2003-10-15	Nettoyage argument de nil	herbelin
2003-10-14	Changement 'as notation' en 'where notation'	herbelin
2003-10-14	Argument de except, error implicite seulement en v8; Changement 'as notation'...	herbelin
2003-10-14	Argument de None implicite seulement en v8	herbelin
2003-10-13	Argument implicite pour None, error, except	herbelin
2003-10-13	Notations pour l'exponentiation	herbelin
2003-10-13	Enregistrement '^' en v8	herbelin
2003-10-11	mise a jour nouvelle syntaxe	barras
2003-10-10	nat_scope ouvert par defaut	herbelin
2003-10-10	identity est equivalent sur Type (sauf sans argument)	herbelin
2003-10-10	type_scope	herbelin
2003-10-10	Suppression de definitions equivalentes	herbelin
2003-10-10	Notation '^'	herbelin