aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/FSets/FSetAVL.v
Commit message (Expand)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Nicer names: DecidableType2* --> Equalities*, OrderedType2* --> Orders*Gravatar letouzey2010-01-07
* FSetCompat: a compatibility wrapper between FSets and MSetsGravatar letouzey2009-10-20
* Merge SetoidList2 into SetoidList.Gravatar letouzey2009-10-19
* Fix the stdlib doc compilation + switch all .v file to utf8Gravatar letouzey2009-09-28
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* FSet/OrderedType now includes an eq_dec, and hence become an extension of Dec...Gravatar letouzey2008-12-17
* Prevent the apparition of &&& when printing a (if ... then ... else false)Gravatar letouzey2008-04-17
* Rework of FMapAVL inspired by recent changes of FSetAVL: Gravatar letouzey2008-04-03
* - notations &&& and ||| equivalent to andb and orb, Gravatar letouzey2008-03-27
* One more AVL reorganisation: separate pure functions from proofs + functional...Gravatar letouzey2008-03-21
* Some "if then else" instead of orb and andb, in order to vm_compute lazilyGravatar letouzey2008-03-21
* still some useless invariants in FSetAVLGravatar letouzey2008-03-20
* migration of the old IntMap library from StdLib to a user contrib (Cachan/Int...Gravatar letouzey2008-03-19
* Reorganisation of FSetAVL (consequences of remarks by B. Gregoire)Gravatar letouzey2008-03-15
* repair FSets/FMap after the change in setoid rewriteGravatar letouzey2008-03-07
* migration from Set to Type of FSet/FMap + some dependencies...Gravatar letouzey2008-03-04
* Nicer third spec of choose. Gravatar letouzey2008-02-28
* For more uniformity, use implicits in FSetAVLGravatar letouzey2008-02-27
* Major revision of FSetAVL: more Function, including some non-structural onesGravatar letouzey2008-02-09
* kill some useless module aliases E:=X (for better name printing, see Elie's 1...Gravatar letouzey2008-02-05
* Revision of the FSetWeak Interface, so that it becomes a precise Gravatar letouzey2007-10-29
* A generic preprocessing tactic zify for (r)omegaGravatar letouzey2007-07-18
* Deletion of some firstorder calls in FSetAVL: Gravatar letouzey2007-07-13
* * 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 00:34:25 +0000