aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
2003-06-10Deplacement delimiteur T dans Notationsherbelin
2003-05-29Bug niveauherbelin
2003-05-29niveau 49 devient nextherbelin
2003-05-29niveau 49 devient nextherbelin
2003-05-29Ne pas mettre d'associatif a droite au niveau 3 en V7herbelin
2003-05-27'only parsing' pour le passage de trucT a trucherbelin
2003-05-24"INZ" déplacé en V8 dans ZArith, juste syntaxique en V7 dans Realsherbelin
2003-05-22V8Notationherbelin
2003-05-22Ajout V8Notationherbelin
2003-05-21Concentration des notations officielles dans Init/Notations; restructuration ...herbelin
2003-05-21Notationsherbelin
2003-05-21Bugherbelin
2003-05-14Amelioration presentationherbelin
2003-05-14Amelioration affichageherbelin
2003-05-14Suppression de 'R' dans la notation == entreherbelin
2003-05-14Suppression de 'R' dans la notation == entreherbelin
2003-05-14Deplacement lemmes sur fact de Reals vers Arithherbelin
2003-05-13Nouveaux lemmesherbelin
2003-05-13Nouveaux lemmes (sur proposition de Nijmegen)herbelin
2003-05-13Nouveaux lemmes (sur proposition de Nijmegen)herbelin
2003-05-09ajout inverse relation bien fondeemohring
2003-05-07coqide: toolbar/autosavemonate
2003-04-29Blancsherbelin
2003-04-29Notationsherbelin
2003-04-29Implicit Typesherbelin
2003-04-29Ajout ChoiceFactsherbelin
2003-04-29Blancsherbelin
2003-04-29En v8: abandon de Rle_sym2, Rle_sym1 au profit de Rge_le, Rle_ge; abandon de ...herbelin
2003-04-28Un principe light d'elimination de Acc, suivant les remarques de Yves Bertotletouzey
2003-04-17Intégration DatatypesSyntax à Datatypesherbelin
2003-04-17Diversherbelin
2003-04-17<> maintenant standardherbelin
2003-04-17Intégration DatatypesSyntax à Datatypesherbelin
2003-04-17Syntaxe 'x=y:>T'herbelin
2003-04-16suite au commit d'hugo dans TypeSyntax & Raxiom, Intro donnait un nom differentletouzey
2003-04-16sumboolT, sumorT, sigTT, SigT redondantsherbelin
2003-04-14Cosmetiqueherbelin
2003-04-14Local 'o'herbelin
2003-04-12Open Scope en Localherbelin
2003-04-10Open Scope remplace Importherbelin
2003-04-10Calcul automatique de l'implicite de nil pour que l'affichage sache le traiterherbelin
2003-04-10Remplacement Import par Open Scope en v8herbelin
2003-04-09cast de nilherbelin
2003-04-09nil en implicite dans la v8herbelin
2003-04-09Ajout Open Scopeherbelin
2003-04-09Activation des implicites pour la v8herbelin
2003-04-09Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"herbelin
2003-04-09Renommage K; equivalence JMeq et eq_dep sur Typeherbelin
2003-04-09Definedherbelin
2003-04-09Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import".herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-17 23:09:38 +0000