aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
2003-11-07Oubli BinNatherbelin
2003-11-07Oubli d'un Set Implicit Argumentsherbelin
2003-11-07Biblio standard sans mention de la possibilite d'etre impredicatifherbelin
2003-11-07Biblio standard sans impredicativiteherbelin
2003-11-06Des oublisherbelin
2003-11-06Report des definitions sorties de fast_integer pour compatibiliteherbelin
2003-11-05Notationsherbelin
2003-11-05Ajout répertoire NArith pour l'arithmétique binaire sur les nombres positif...herbelin
2003-11-05Preuve de l'incoherence de {A}+{~A} avec Set impredicatifherbelin
2003-11-05Redondancesherbelin
2003-11-05Restructuration ZArith et déport de la partie sur 'positive' dans NArith, de...herbelin
2003-11-03Exporting ^; utilisation arg scope impliciteherbelin
2003-11-02Cosmetiqueherbelin
2003-11-02Renforcement significatif du resultat principalherbelin
2003-11-02Rien de bien importantherbelin
2003-11-02Commentairesherbelin
2003-11-02Typoherbelin
2003-11-02AC + EXT -> EMherbelin
2003-11-02Relations entre le choix (forme relationnelle) avec restriction ou nonherbelin
2003-11-02Renommage bool en boolP pour eviter la qualificationherbelin
2003-11-02Restauration preference Rge a Rle pour compatibilite...herbelin
2003-11-02Restauration preference Rge a Rle pour compatibilite...; petit nettoyageherbelin
2003-11-01Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les entie...herbelin
2003-11-01Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les entie...herbelin
2003-10-30Parsing du moins unaire au niveau de l'application qui n'a pas besoin d'etre ...herbelin
2003-10-29Choix sous sa forme relationnelleherbelin
2003-10-28Ordre (symbolique) des Requireherbelin
2003-10-28Passage de la notations de paire dans core_scopeherbelin
2003-10-28Passage des notations de type dans type_scopeherbelin
2003-10-28Ajout %core; MAJ niveau connecteurs logiqueherbelin
2003-10-28MAJherbelin
2003-10-28Fichier offrant l'axiome du choix unique en presence de logique classiqueherbelin
2003-10-28Fichier offrant l'axiome du choix en presence de logique classiqueherbelin
2003-10-28La logique sur Type inclut celle sur Setherbelin
2003-10-28Retour en arriere sur d'autres renommages de variablesherbelin
2003-10-27Retour a un nommage non standard des variables pour compatibilite; report 're...herbelin
2003-10-27Bug du commit precedentherbelin
2003-10-23Commentairesherbelin
2003-10-22Documentation/Structurationherbelin
2003-10-22Documentation/Structurationherbelin
2003-10-22reorganisation des niveaux (ex: = est a 70)barras
2003-10-21Redondance de dec_eq_natherbelin
2003-10-21Type relation dans Datatypesherbelin
2003-10-21Maintenant avant Datatypesherbelin
2003-10-21ajoutsherbelin
2003-10-20R passe dans Set !herbelin
2003-10-1720 est uniquement associatif a gaucheherbelin
2003-10-17Des implicites plus 'naturels' pour eq_ind, identity_ind and coherbelin
2003-10-16nouvelle syntaxe de ltacbarras
2003-10-16lettac -> setbarras
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 18:35:36 +0000