index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
theories
/
FSets
/
FSetAVL.v
Commit message (
Expand
)
Author
Age
*
Prevent the apparition of &&& when printing a (if ... then ... else false)
letouzey
2008-04-17
*
Rework of FMapAVL inspired by recent changes of FSetAVL:
letouzey
2008-04-03
*
- notations &&& and ||| equivalent to andb and orb,
letouzey
2008-03-27
*
One more AVL reorganisation: separate pure functions from proofs + functional...
letouzey
2008-03-21
*
Some "if then else" instead of orb and andb, in order to vm_compute lazily
letouzey
2008-03-21
*
still some useless invariants in FSetAVL
letouzey
2008-03-20
*
migration of the old IntMap library from StdLib to a user contrib (Cachan/Int...
letouzey
2008-03-19
*
Reorganisation of FSetAVL (consequences of remarks by B. Gregoire)
letouzey
2008-03-15
*
repair FSets/FMap after the change in setoid rewrite
letouzey
2008-03-07
*
migration from Set to Type of FSet/FMap + some dependencies...
letouzey
2008-03-04
*
Nicer third spec of choose.
letouzey
2008-02-28
*
For more uniformity, use implicits in FSetAVL
letouzey
2008-02-27
*
Major revision of FSetAVL: more Function, including some non-structural ones
letouzey
2008-02-09
*
kill some useless module aliases E:=X (for better name printing, see Elie's 1...
letouzey
2008-02-05
*
Revision of the FSetWeak Interface, so that it becomes a precise
letouzey
2007-10-29
*
A generic preprocessing tactic zify for (r)omega
letouzey
2007-07-18
*
Deletion of some firstorder calls in FSetAVL:
letouzey
2007-07-13
*
* For uniformity, FSetAVL uses Implicit Arguments (a bit)
letouzey
2007-06-07
*
As suggested by Pierre Casteran, fold for FSets/FMaps now takes a
letouzey
2007-05-27
*
fix for bug #1347 (no more Scope pollution by FSets)
letouzey
2007-05-25
*
FSetInterface: new item choose_equal in the spec S (request of P. Casteran)
letouzey
2007-02-28
*
Passage des graphes de Function dans Type
jforest
2006-06-23
*
+ ameliorating the tactic "functional induction"
jforest
2006-06-06
*
Replacing the old version of "functional induction" with the new one.
jforest
2006-05-31
*
Suite changement précédence by de assert
herbelin
2006-05-24
*
suite des marquages de types et opacifications de lemmes dans les wrappers Make
letouzey
2006-05-22
*
suite tentative pour permettre l'utilisation de modules de FSets
letouzey
2006-05-20
*
suite de l'ajout des FSets/FMaps dans les theories standards
letouzey
2006-04-29
*
suppression de FSets (redevient une contrib)
filliatr
2003-06-24
*
doc
filliatr
2003-06-24
*
concat; debut split
filliatr
2003-06-24
*
join
filliatr
2003-06-23
*
add_tree : sur type tree plutot que sur type t
filliatr
2003-06-23
*
merge_bis et debug join
filliatr
2003-06-23
*
remov
filliatr
2003-06-20
*
merge
filliatr
2003-06-20
*
remove_min, remove_max
filliatr
2003-06-20
*
add
filliatr
2003-06-19
*
bal: preuve terminee
filliatr
2003-06-19
*
bal: premier cas hl > hr + 2
filliatr
2003-06-19
*
typo
filliatr
2003-06-19
*
AVL: suite
filliatr
2003-06-18
*
AVL: suite
filliatr
2003-06-17
*
AVL de caml: un debut
filliatr
2003-06-17