aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
2003-06-20removfilliatr
2003-06-20mergefilliatr
2003-06-20remove_min, remove_maxfilliatr
2003-06-19addfilliatr
2003-06-19bal: preuve termineefilliatr
2003-06-19bal: premier cas hl > hr + 2filliatr
2003-06-19typofilliatr
2003-06-18AVL: suitefilliatr
2003-06-18Arguments superflus pour Zlength_nilherbelin
2003-06-17AVL: suitefilliatr
2003-06-17AVL de caml: un debutfilliatr
2003-06-16Ground depthfilliatr
2003-06-16reparation fsets suite a changement de Groundfilliatr
2003-06-14Deplacement de le_minus de fast_integer vers Minusherbelin
2003-06-14Deplacement de le_minus de fast_integer vers Minusherbelin
2003-06-13changement de spécif du foldletouzey
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 01:40:19 +0000