aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
2003-06-13fcts tail-recursivesfilliatr
2003-06-13Require Exportfilliatr
2003-06-13FSets, mais pas compile' par make worldfilliatr
2003-06-13suite changements ZArith en vu de librairie FSetletouzey
2003-06-13quelques adaptations de Zarith en vu de la nouvelle librarie FSetletouzey
2003-06-13Deplacement d'un lemme sur nat de ZArith vers Arithherbelin
2003-06-12INZ reste constante pour compat V7 mais Unfold INZ est supprimé par le tradu...herbelin
2003-06-10Import nat_scopeherbelin
2003-06-10Suppression d'une occurrence superflue d'argument de type dans Notation sacha...herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 21:16:55 +0000