aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/FSets/FSetAVL.v
Commit message (Expand)AuthorAge
* + ameliorating the tactic "functional induction"Gravatar jforest2006-06-06
* Replacing the old version of "functional induction" with the new one. Gravatar jforest2006-05-31
* Suite changement précédence by de assertGravatar herbelin2006-05-24
* suite des marquages de types et opacifications de lemmes dans les wrappers MakeGravatar letouzey2006-05-22
* suite tentative pour permettre l'utilisation de modules de FSetsGravatar letouzey2006-05-20
* suite de l'ajout des FSets/FMaps dans les theories standardsGravatar letouzey2006-04-29
* suppression de FSets (redevient une contrib)Gravatar filliatr2003-06-24
* docGravatar filliatr2003-06-24
* concat; debut splitGravatar filliatr2003-06-24
* joinGravatar filliatr2003-06-23
* add_tree : sur type tree plutot que sur type tGravatar filliatr2003-06-23
* merge_bis et debug joinGravatar filliatr2003-06-23
* removGravatar filliatr2003-06-20
* mergeGravatar filliatr2003-06-20
* remove_min, remove_maxGravatar filliatr2003-06-20
* addGravatar filliatr2003-06-19
* bal: preuve termineeGravatar filliatr2003-06-19
* bal: premier cas hl > hr + 2Gravatar filliatr2003-06-19
* typoGravatar filliatr2003-06-19
* AVL: suiteGravatar filliatr2003-06-18
* AVL: suiteGravatar filliatr2003-06-17
* AVL de caml: un debutGravatar filliatr2003-06-17