aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/FSets/FMapAVL.v
Commit message (Expand)AuthorAge
* kill some useless module aliases E:=X (for better name printing, see Elie's 1...Gravatar letouzey2008-02-05
* small tactics "swap" and "absurd_hyp" are now obsolete: "contradict" is Gravatar letouzey2007-11-06
* 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
* 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
* 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 de la revision des wrappers MakeGravatar letouzey2006-05-30
* suite de l'ajout des FSets/FMaps dans les theories standardsGravatar letouzey2006-04-29