aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/FSets/FSetAVL.v
Commit message (Expand)AuthorAge
* * For uniformity, FSetAVL uses Implicit Arguments (a bit)Gravatar letouzey2007-06-07
* As suggested by Pierre Casteran, fold for FSets/FMaps now takes a Gravatar letouzey2007-05-27
* fix for bug #1347 (no more Scope pollution by FSets)Gravatar letouzey2007-05-25
* FSetInterface: new item choose_equal in the spec S (request of P. Casteran)Gravatar letouzey2007-02-28
* Passage des graphes de Function dans Type Gravatar jforest2006-06-23
* + 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 16:01:40 +0000