aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/FSets
Commit message (Expand)AuthorAge
* Final part of moving Program code inside the main code. Adapted add_definitio...Gravatar msozeau2012-03-14
* Revert "Tentative to fix bug #2628 by not letting intuition break records. Mi...Gravatar msozeau2012-01-31
* Tentative to fix bug #2628 by not letting intuition break records. Might be t...Gravatar msozeau2012-01-28
* theories/, plugins/ and test-suite/ ported to the Arguments vernacularGravatar gareuselesinge2011-11-21
* MSet/FSet/FMap : add more explicitly an alternative spec for fold via fold_rightGravatar letouzey2011-10-14
* fsetdec : non-atomic elements are now transformed as variables first (fix #2464)Gravatar letouzey2011-10-07
* Improved handling of element equalities in fsetdec (fix #2467)Gravatar letouzey2011-10-07
* Modularization of BinInt, related fixes in the stdlibGravatar letouzey2011-05-05
* - Add modulo_delta_types flag for unification to allow fullGravatar msozeau2011-03-13
* - Use transparency information all the way through unification andGravatar msozeau2011-02-17
* Fix compilation issues.Gravatar msozeau2011-02-16
* - Fix treatment of globality flag for typeclass instance hints (theyGravatar msozeau2011-02-14
* s/appartness/membership/g (Closes: #2470)Gravatar glondu2011-01-06
* Cosmetic : let's take advantage of the n-ary exists notationGravatar letouzey2010-12-17
* FMapFacts: typo noticed by AaronGravatar letouzey2010-10-22
* Extraction: re-introduce some eta-expansions in rare situations leading to '_...Gravatar letouzey2010-09-20
* For the moment, two small manual eta-expansions to avoid '_a after extractionGravatar letouzey2010-09-17
* Reverted 13293 commited mistakenly. Sorry for the noise.Gravatar herbelin2010-07-18
* Tentative de suppression de l'import automatique des hints et coercions.Gravatar herbelin2010-07-18
* FSetPositive: sets of positive inspired by FMapPositive.Gravatar letouzey2010-07-16
* FSets/Msets: some renaming of module params to simplify the task of the extra...Gravatar letouzey2010-07-05
* fsetdec: a forgotten Set instead of Type was breaking discard_nonFset (fix #2...Gravatar letouzey2010-06-18
* fsetdec: clear dependent hypothesis before anything else (fix #2136).Gravatar letouzey2010-06-17
* Made option "Automatic Introduction" active by default before too manyGravatar herbelin2010-06-08
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* CompSpecType, a clone of CompSpec but in Type instead of PropGravatar letouzey2010-02-12
* Nicer names: DecidableType2* --> Equalities*, OrderedType2* --> Orders*Gravatar letouzey2010-01-07
* Include can accept both Module and Module TypeGravatar letouzey2010-01-07
* Factorisation between Makefile and ocamlbuild systems : .vo to compile are in...Gravatar letouzey2009-12-09
* Better visibility of the inductive CompSpec used to specify comparison functionsGravatar letouzey2009-11-03
* OrderedType implementation for various numerical datatypes + min/max structuresGravatar letouzey2009-11-03
* List + SetoidList : some cleanup around predicates Exists, Forall, Forall2, F...Gravatar letouzey2009-11-02
* Remove various useless {struct} annotationsGravatar letouzey2009-11-02
* FSetCompat: a compatibility wrapper between FSets and MSetsGravatar letouzey2009-10-20
* Merge SetoidList2 into SetoidList.Gravatar letouzey2009-10-19
* Structure/OrderTac.v : highlight the "order" tactic by isolating it from FSet...Gravatar letouzey2009-10-16
* MSets: a new generation of FSetsGravatar letouzey2009-10-13
* Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'Gravatar letouzey2009-10-08
* Implicit argument of Logic.eq become maximally insertedGravatar letouzey2009-10-08
* Fix the stdlib doc compilation + switch all .v file to utf8Gravatar letouzey2009-09-28
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Znumtheory + Zdiv enriched with stuff from ZMicromega, misc improvementsGravatar letouzey2009-09-09
* Fix the bug-ridden code used to choose leibniz or generalizedGravatar msozeau2009-09-08
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-19 09:26:57 +0000