aboutsummaryrefslogtreecommitdiff
path: root/theories/FSets
AgeCommit message (Expand)Author
2008-09-14Add user syntax for creating hint databases [Create HintDb foomsozeau
2008-09-04Correction du bug #1937notin
2008-06-27Enhanced discrimination nets implementation, which can now work withmsozeau
2008-06-06avoid duplicated creation of WFacts instancesletouzey
2008-06-01Intropattern: syntax {x,y,z,t} becomes (x & y & z & t), as decided inletouzey
2008-04-17Prevent the apparition of &&& when printing a (if ... then ... else false)letouzey
2008-04-12Add the ability to specify what to do with free variables in instancemsozeau
2008-04-08- A little cleanup in Classes/*. Separate standard morphisms onmsozeau
2008-04-03New file FMapFullAVL containing the balancing proofs about FMapAVL:letouzey
2008-04-03Rework of FMapAVL inspired by recent changes of FSetAVL: letouzey
2008-03-27- notations &&& and ||| equivalent to andb and orb, letouzey
2008-03-21One more AVL reorganisation: separate pure functions from proofs + functional...letouzey
2008-03-21Some "if then else" instead of orb and andb, in order to vm_compute lazilyletouzey
2008-03-20still some useless invariants in FSetAVLletouzey
2008-03-19migration of the old IntMap library from StdLib to a user contrib (Cachan/Int...letouzey
2008-03-19Do another pass on the typeclasses code. Correct globalization of classmsozeau
2008-03-16Reorganize Program and Classes theories. Requiring Setoid no longer setsmsozeau
2008-03-15Reorganisation of FSetAVL (consequences of remarks by B. Gregoire)letouzey
2008-03-07f_equal, revert, specialize in ML, contradict in better Ltac (+doc)letouzey
2008-03-07repair FSets/FMap after the change in setoid rewriteletouzey
2008-03-06Plug the new setoid implemtation in, leaving the original one commentedmsozeau
2008-03-04migration from Set to Type of FSet/FMap + some dependencies...letouzey
2008-03-02A fix for compilation of FMapFacts (a story of impl arg for Logic.eq)letouzey
2008-02-28Some suggestions about FMap by P. Casteran: letouzey
2008-02-28cardinal is promoted to the rank of primitive member of the FMap interfaceletouzey
2008-02-28Nicer third spec of choose. letouzey
2008-02-27For more uniformity, use implicits in FSetAVLletouzey
2008-02-10Major revision: use of Function, including some non-structural onesletouzey
2008-02-09Major revision of FSetAVL: more Function, including some non-structural onesletouzey
2008-02-08misc improvementsletouzey
2008-02-08better comments in FMapInterfaceletouzey
2008-02-08better comments in FSetInterfaceletouzey
2008-02-08more complete FSets.vletouzey
2008-02-05kill some useless module aliases E:=X (for better name printing, see Elie's 1...letouzey
2008-02-04Reorganization of FSet+FMap : no more files specific to Weak Sets/Mapsletouzey
2008-02-02factorization part II (Properties + EqProperties), inclusion of FSetDecide (f...letouzey
2008-02-01Thanks to Elie, we can share duplicated stuff in FSets: for a start, FSetWeak...letouzey
2008-01-04more user-friendly versions of some properties lemmas in FSets/FMapletouzey
2007-11-24* A few Parameter Inline, but they dont seem to help much concerning letouzey
2007-11-06small tactics "swap" and "absurd_hyp" are now obsolete: "contradict" is letouzey
2007-10-30temporary workaround for bug #1738letouzey
2007-10-30A useless Add Morphism: since Subset is a Setoid Relation, it is alsoletouzey
2007-10-29Revision of the FSetWeak Interface, so that it becomes a precise letouzey
2007-10-21Cleanup attempt of Hints in *Interface.v files.letouzey
2007-07-18A generic preprocessing tactic zify for (r)omegaletouzey
2007-07-13Deletion of some firstorder calls in FSetAVL: letouzey
2007-06-27- Extensions of FMap(Weak)Facts: letouzey
2007-06-26additional properties for FMap (and slight rework of SetoidList and FSetPrope...letouzey
2007-06-14Rework of FSetProperties, in order to add more easily a Properties functor letouzey
2007-06-11undeletion of E_ST and Equal_ST: these records aren't mandatory, but quite us...letouzey