coq - The formal proof system

Age	Commit message (Expand)	Author
2003-11-12	%type au lieu de %T	herbelin
2003-11-12	Lemmes dans un sens plus naturel	herbelin
2003-11-12	Restructuration ZArith	herbelin
2003-11-12	Cosmetique	herbelin
2003-11-12	Noms canoniques pour les variables liees	herbelin
2003-11-12	Independance vis a vis noms variables liees; partie sur bool dans Zbool	herbelin
2003-11-12	Noms/énoncés plus canoniques	herbelin
2003-11-12	Independance vis a vis noms variables liees	herbelin
2003-11-12	Ajout lemmes; independance vis a vis noms variables liees; restructuration	herbelin
2003-11-12	Ajout partie sur bool anciennement dans Zmisc	herbelin
2003-11-12	Ajout lemmes; independance vis a vis noms variables liees	herbelin
2003-11-12	On sait jamais	herbelin
2003-11-12	petits changements de syntaxe	barras
2003-11-09	Ajout quelques lemmes; noms des variables liees	herbelin
2003-11-07	Oubli BinNat	herbelin
2003-11-07	Oubli d'un Set Implicit Arguments	herbelin
2003-11-07	Biblio standard sans mention de la possibilite d'etre impredicatif	herbelin
2003-11-07	Biblio standard sans impredicativite	herbelin
2003-11-06	Des oublis	herbelin
2003-11-06	Report des definitions sorties de fast_integer pour compatibilite	herbelin
2003-11-05	Notations	herbelin
2003-11-05	Ajout répertoire NArith pour l'arithmétique binaire sur les nombres positif...	herbelin
2003-11-05	Preuve de l'incoherence de {A}+{~A} avec Set impredicatif	herbelin
2003-11-05	Redondances	herbelin
2003-11-05	Restructuration ZArith et déport de la partie sur 'positive' dans NArith, de...	herbelin
2003-11-03	Exporting ^; utilisation arg scope implicite	herbelin
2003-11-02	Cosmetique	herbelin
2003-11-02	Renforcement significatif du resultat principal	herbelin
2003-11-02	Rien de bien important	herbelin
2003-11-02	Commentaires	herbelin
2003-11-02	Typo	herbelin
2003-11-02	AC + EXT -> EM	herbelin
2003-11-02	Relations entre le choix (forme relationnelle) avec restriction ou non	herbelin
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