aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
2003-09-12Suppression DatatypesSyntax et PeanoSyntax qui était videsherbelin
2003-09-12Ajout et MAJ commandes de scopesherbelin
2003-09-12Bind et Delimit pour Rherbelin
2003-09-12Bind et Delimit pour natherbelin
2003-09-12Bind et Delimit pour positive et Z (hors section)herbelin
2003-09-12Bind et Delimit pour Rherbelin
2003-09-11Suppression notations redondantes en v8 : Fst, ProjS1, Value, Ex ...herbelin
2003-09-05principes de récurrences plus efficaces pour l'extractionletouzey
2003-09-05Zdiv plus efficace: r+r -> 2*rletouzey
2003-09-05Zabs_Zsgnletouzey
2003-09-01Passage de 'relation' à Typeherbelin
2003-08-10Affichage {}+{}, niveau paire au plus hautherbelin
2003-08-10Un peu d'aide pour le traducteurherbelin
2003-07-18Coq.Init.Logic.eq au lieu de eqfilliatr
2003-07-08recursion bien fondee sur des pairsfilliatr
2003-06-24suppression de FSets (redevient une contrib)filliatr
2003-06-24docfilliatr
2003-06-24concat; debut splitfilliatr
2003-06-23joinfilliatr
2003-06-23add_tree : sur type tree plutot que sur type tfilliatr
2003-06-23merge_bis et debug joinfilliatr
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