aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/FSets
Commit message (Expand)AuthorAge
* instanciation is French, instantiation is EnglishGravatar Jason Gross2014-08-25
* Grammar: "allowing to" is not proper EnglishGravatar Jason Gross2014-08-25
* More proofs independent of the names generated by induction/elim overGravatar Hugo Herbelin2014-08-05
* Adding a generalized version of fold_Equal to FMapFacts.Gravatar Pierre Courtieu2014-07-31
* Avoid using a deprecated lemma in the standard library.Gravatar Guillaume Melquiond2014-06-26
* Cleanup treatment of template universe polymorphism (thanks to E. TassiGravatar Matthieu Sozeau2014-06-20
* Make standard library independent of the names generated byGravatar Hugo Herbelin2014-06-04
* Making those proofs which depend on names generated for the argumentsGravatar Hugo Herbelin2014-06-01
* Fix after merge.Gravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Cbn is happier when ?SetPositive fixpoints have the set as recursive argumentGravatar Pierre Boutillier2014-05-02
* Eta contractions to please cbnGravatar Pierre Boutillier2014-05-02
* "Boolean Equality" and "Case Analysis" are already off by default...Gravatar letouzey2013-07-17
* Unset Asymmetric PatternsGravatar pboutill2013-01-18
* No more constant named "int" in Coq theories (cf bug #2878)Gravatar letouzey2012-12-18
* Ltac repeat is in fact already doing progressGravatar letouzey2012-10-01
* Kills the useless tactic annotations "in |- *"Gravatar letouzey2012-07-05
* Open Local Scope ---> Local Open Scope, same with Notation and aliiGravatar letouzey2012-07-05
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* 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
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-23 02:34:17 +0000