aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/FSets
Commit message (Expand)AuthorAge
...
* Better compatibility after commit 11693 by adding an alias OrderedTypeFacts.e...Gravatar letouzey2008-12-17
* FSet/OrderedType now includes an eq_dec, and hence become an extension of Dec...Gravatar letouzey2008-12-17
* Structural definition of PositiveMap.foldGravatar glondu2008-12-11
* Make PositiveMap.xmapi structuralGravatar glondu2008-12-11
* integrate suggestions by B. Baydemir (see #1930)Gravatar letouzey2008-11-17
* Port [rewrite] tactics to open terms. Currently no check that evarsGravatar msozeau2008-11-05
* Add user syntax for creating hint databases [Create HintDb fooGravatar msozeau2008-09-14
* Correction du bug #1937Gravatar notin2008-09-04
* Enhanced discrimination nets implementation, which can now work withGravatar msozeau2008-06-27
* avoid duplicated creation of WFacts instancesGravatar letouzey2008-06-06
* Intropattern: syntax {x,y,z,t} becomes (x & y & z & t), as decided inGravatar letouzey2008-06-01
* Prevent the apparition of &&& when printing a (if ... then ... else false)Gravatar letouzey2008-04-17
* Add the ability to specify what to do with free variables in instanceGravatar msozeau2008-04-12
* - A little cleanup in Classes/*. Separate standard morphisms onGravatar msozeau2008-04-08
* New file FMapFullAVL containing the balancing proofs about FMapAVL:Gravatar letouzey2008-04-03
* 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
* Do another pass on the typeclasses code. Correct globalization of classGravatar msozeau2008-03-19
* Reorganize Program and Classes theories. Requiring Setoid no longer setsGravatar msozeau2008-03-16
* Reorganisation of FSetAVL (consequences of remarks by B. Gregoire)Gravatar letouzey2008-03-15
* f_equal, revert, specialize in ML, contradict in better Ltac (+doc)Gravatar letouzey2008-03-07
* repair FSets/FMap after the change in setoid rewriteGravatar letouzey2008-03-07
* Plug the new setoid implemtation in, leaving the original one commentedGravatar msozeau2008-03-06
* migration from Set to Type of FSet/FMap + some dependencies...Gravatar letouzey2008-03-04
* A fix for compilation of FMapFacts (a story of impl arg for Logic.eq)Gravatar letouzey2008-03-02
* Some suggestions about FMap by P. Casteran: Gravatar letouzey2008-02-28
* cardinal is promoted to the rank of primitive member of the FMap interfaceGravatar letouzey2008-02-28
* Nicer third spec of choose. Gravatar letouzey2008-02-28
* For more uniformity, use implicits in FSetAVLGravatar letouzey2008-02-27
* Major revision: use of Function, including some non-structural onesGravatar letouzey2008-02-10
* Major revision of FSetAVL: more Function, including some non-structural onesGravatar letouzey2008-02-09
* misc improvementsGravatar letouzey2008-02-08
* better comments in FMapInterfaceGravatar letouzey2008-02-08
* better comments in FSetInterfaceGravatar letouzey2008-02-08
* more complete FSets.vGravatar letouzey2008-02-08
* kill some useless module aliases E:=X (for better name printing, see Elie's 1...Gravatar letouzey2008-02-05
* Reorganization of FSet+FMap : no more files specific to Weak Sets/MapsGravatar letouzey2008-02-04
* factorization part II (Properties + EqProperties), inclusion of FSetDecide (f...Gravatar letouzey2008-02-02
* Thanks to Elie, we can share duplicated stuff in FSets: for a start, FSetWeak...Gravatar letouzey2008-02-01
* more user-friendly versions of some properties lemmas in FSets/FMapGravatar letouzey2008-01-04
* * A few Parameter Inline, but they dont seem to help much concerning Gravatar letouzey2007-11-24
* small tactics "swap" and "absurd_hyp" are now obsolete: "contradict" is Gravatar letouzey2007-11-06
* temporary workaround for bug #1738Gravatar letouzey2007-10-30
* A useless Add Morphism: since Subset is a Setoid Relation, it is alsoGravatar letouzey2007-10-30
* Revision of the FSetWeak Interface, so that it becomes a precise Gravatar letouzey2007-10-29
* Cleanup attempt of Hints in *Interface.v files.Gravatar letouzey2007-10-21
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-14 23:52:43 +0000