aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/FSets
Commit message (Expand)AuthorAge
* OrderedTypeEx.N_as_OT use Nlt, various minor improvements in N/ZArithGravatar letouzey2009-07-24
* Better comparison functions in OrderedTypeExGravatar letouzey2009-07-22
* Simplify eauto and fix it for compatibility, allowing full delta duringGravatar msozeau2009-07-14
* Use the proper unification flags in e_exact. This makes exact fail a bitGravatar msozeau2009-07-09
* made several occurrences of (eapply ...; eauto) not rely on the lack of patte...Gravatar barras2009-06-22
* Rename [Morphism] into [Proper] and [respect] into [proper] to complyGravatar msozeau2009-04-21
* Just export RelationClasses for [Equivalence] through Setoid.Gravatar msozeau2009-04-18
* ZArith/Int: no need to load romega here (but rather in FullAVL)Gravatar letouzey2009-03-28
* FSet(Weak)List : eq_dec becomes Defined (and gets better proof)Gravatar letouzey2009-01-28
* Switched to "standardized" names for the properties of eq andGravatar herbelin2009-01-01
* - Another bug in get_sort_family_of (sort-polymorphism of constants andGravatar herbelin2008-12-28
* FMaps: various updates (mostly suggested by P. Casteran)Gravatar letouzey2008-12-26
* FMap: fold_rec + more permissive transpose hyp + various cleanupGravatar letouzey2008-12-22
* FSets: integration of suggestions by P. Casteran and S. LescuyerGravatar letouzey2008-12-18
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-14 07:16:17 +0000