aboutsummaryrefslogtreecommitdiff
path: root/theories/FSets
AgeCommit message (Expand)Author
2014-08-25Grammar: "allowing to" is not proper EnglishJason Gross
2014-08-05More proofs independent of the names generated by induction/elim overHugo Herbelin
2014-07-31Adding a generalized version of fold_Equal to FMapFacts.Pierre Courtieu
2014-06-26Avoid using a deprecated lemma in the standard library.Guillaume Melquiond
2014-06-20Cleanup treatment of template universe polymorphism (thanks to E. TassiMatthieu Sozeau
2014-06-04Make standard library independent of the names generated byHugo Herbelin
2014-06-01Making those proofs which depend on names generated for the argumentsHugo Herbelin
2014-05-06Fix after merge.Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-05-02Cbn is happier when ?SetPositive fixpoints have the set as recursive argumentPierre Boutillier
2014-05-02Eta contractions to please cbnPierre Boutillier
2013-07-17"Boolean Equality" and "Case Analysis" are already off by default...letouzey
2013-01-18Unset Asymmetric Patternspboutill
2012-12-18No more constant named "int" in Coq theories (cf bug #2878)letouzey
2012-10-01Ltac repeat is in fact already doing progressletouzey
2012-07-05Kills the useless tactic annotations "in |- *"letouzey
2012-07-05Open Local Scope ---> Local Open Scope, same with Notation and aliiletouzey
2012-07-05ZArith + other : favor the use of modern names instead of compat notationsletouzey
2012-05-15Intuition: temporary(?) restore the unconditional unfolding of notletouzey
2012-04-15Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).herbelin
2012-03-14Final part of moving Program code inside the main code. Adapted add_definitio...msozeau
2012-01-31Revert "Tentative to fix bug #2628 by not letting intuition break records. Mi...msozeau
2012-01-28Tentative to fix bug #2628 by not letting intuition break records. Might be t...msozeau
2011-11-21theories/, plugins/ and test-suite/ ported to the Arguments vernaculargareuselesinge
2011-10-14MSet/FSet/FMap : add more explicitly an alternative spec for fold via fold_rightletouzey
2011-10-07fsetdec : non-atomic elements are now transformed as variables first (fix #2464)letouzey
2011-10-07Improved handling of element equalities in fsetdec (fix #2467)letouzey
2011-05-05Modularization of BinInt, related fixes in the stdlibletouzey
2011-03-13- Add modulo_delta_types flag for unification to allow fullmsozeau
2011-02-17- Use transparency information all the way through unification andmsozeau
2011-02-16Fix compilation issues.msozeau
2011-02-14- Fix treatment of globality flag for typeclass instance hints (theymsozeau
2011-01-06s/appartness/membership/g (Closes: #2470)glondu
2010-12-17Cosmetic : let's take advantage of the n-ary exists notationletouzey
2010-10-22FMapFacts: typo noticed by Aaronletouzey
2010-09-20Extraction: re-introduce some eta-expansions in rare situations leading to '_...letouzey
2010-09-17For the moment, two small manual eta-expansions to avoid '_a after extractionletouzey
2010-07-18Reverted 13293 commited mistakenly. Sorry for the noise.herbelin
2010-07-18Tentative de suppression de l'import automatique des hints et coercions.herbelin
2010-07-16FSetPositive: sets of positive inspired by FMapPositive.letouzey
2010-07-05FSets/Msets: some renaming of module params to simplify the task of the extra...letouzey
2010-06-18fsetdec: a forgotten Set instead of Type was breaking discard_nonFset (fix #2...letouzey
2010-06-17fsetdec: clear dependent hypothesis before anything else (fix #2136).letouzey
2010-06-08Made option "Automatic Introduction" active by default before too manyherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-02-12CompSpecType, a clone of CompSpec but in Type instead of Propletouzey
2010-01-07Nicer names: DecidableType2* --> Equalities*, OrderedType2* --> Orders*letouzey
2010-01-07Include can accept both Module and Module Typeletouzey
2009-12-09Factorisation between Makefile and ocamlbuild systems : .vo to compile are in...letouzey
2009-11-03Better visibility of the inductive CompSpec used to specify comparison functionsletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 21:37:27 +0000