aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/FSets/FMapFacts.v
Commit message (Expand)AuthorAge
* Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-07-07
|\
| * Move option_map notation upGravatar Jason Gross2016-07-05
| * Restore option_map in FMapFactsGravatar Jason Gross2016-07-05
* | Giving a more natural semantics to injection by default.Gravatar Hugo Herbelin2016-06-18
|/
* Fix some typos.Gravatar Guillaume Melquiond2015-12-07
* Adding a generalized version of fold_Equal to FMapFacts.Gravatar Pierre Courtieu2014-07-31
* Making those proofs which depend on names generated for the argumentsGravatar Hugo Herbelin2014-06-01
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Eta contractions to please cbnGravatar Pierre Boutillier2014-05-02
* Intuition: temporary(?) restore the unconditional unfolding of notGravatar letouzey2012-05-15
* Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).Gravatar herbelin2012-04-15
* 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
* Fix compilation issues.Gravatar msozeau2011-02-16
* - Fix treatment of globality flag for typeclass instance hints (theyGravatar msozeau2011-02-14
* Cosmetic : let's take advantage of the n-ary exists notationGravatar letouzey2010-12-17
* FMapFacts: typo noticed by AaronGravatar letouzey2010-10-22
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* List + SetoidList : some cleanup around predicates Exists, Forall, Forall2, F...Gravatar letouzey2009-11-02
* Merge SetoidList2 into SetoidList.Gravatar letouzey2009-10-19
* 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
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Fix the bug-ridden code used to choose leibniz or generalizedGravatar msozeau2009-09-08
* 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
* Rename [Morphism] into [Proper] and [respect] into [proper] to complyGravatar msozeau2009-04-21
* Just export RelationClasses for [Equivalence] through Setoid.Gravatar msozeau2009-04-18
* FMaps: various updates (mostly suggested by P. Casteran)Gravatar letouzey2008-12-26
* FMap: fold_rec + more permissive transpose hyp + various cleanupGravatar letouzey2008-12-22
* FSet/OrderedType now includes an eq_dec, and hence become an extension of Dec...Gravatar letouzey2008-12-17
* 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
* 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
* Reorganize Program and Classes theories. Requiring Setoid no longer setsGravatar msozeau2008-03-16
* 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
* Reorganization of FSet+FMap : no more files specific to Weak Sets/MapsGravatar letouzey2008-02-04
* more user-friendly versions of some properties lemmas in FSets/FMapGravatar letouzey2008-01-04
* small tactics "swap" and "absurd_hyp" are now obsolete: "contradict" is Gravatar letouzey2007-11-06
* Cleanup attempt of Hints in *Interface.v files.Gravatar letouzey2007-10-21
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 03:47:27 +0000