aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Lists
Commit message (Expand)AuthorAge
* Remove some outdated files and fix permissions.Gravatar Guillaume Melquiond2015-07-31
* List.nth_error directly produces Some/None instead of value/errorGravatar Pierre Letouzey2015-05-12
* Giving to "subst" a more natural semantic (fixing #4214) by using allGravatar Hugo Herbelin2015-05-01
* Prove [map_ext] using [map_ext_in].Gravatar Nickolai Zeldovich2015-04-09
* Add a [map_ext_in] lemma to List.v.Gravatar Nickolai Zeldovich2015-04-09
* Introducing MMaps, a modernized FMaps.Gravatar Pierre Letouzey2015-03-04
* Update headers.Gravatar Maxime Dénès2015-01-12
* Use [Proof using] to make sure that [List.in_flat_map] doesn't grab too many ...Gravatar Arnaud Spiwack2014-12-28
* Adds two lemmas about hderror to the List standard library.Gravatar Sébastien Hinderer2014-12-18
* Implement the nodup function on lists and prove associated results.Gravatar Sébastien Hinderer2014-12-18
* Lists: enhanced version of Seb's last commit on Exists/ForallGravatar Pierre Letouzey2014-12-18
* Lists: a few results on Exists and Forall and a bit of code cleanup.Gravatar Sébastien Hinderer2014-12-18
* List.v: sequel to Sebastien's commit (some cosmetics + a few shorter proofs)Gravatar Pierre Letouzey2014-12-11
* First series of results on lists.Gravatar Sébastien Hinderer2014-12-11
* Clarifying the role of ListSet.v in the library, compared to otherGravatar Hugo Herbelin2014-11-18
* Improving printing of "[]" (nil) in spite of the risk of collisionGravatar Hugo Herbelin2014-08-05
* Testing a replacement of "cut" by "enough" on a couple of test files.Gravatar Hugo Herbelin2014-08-05
* 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
* 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
* Try a new way of handling template universe levelsGravatar Matthieu Sozeau2014-05-06
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06
* Correct rebase on STM code. Thanks to E. Tassi for help on dealing withGravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* FinFun.v: results about injective/surjective/bijective fonctions over finite ...Gravatar Pierre Letouzey2014-02-07
* List: Bug 3039 weaker requirement for fold symmetricGravatar Pierre Boutillier2013-12-20
* Added a concat function to List theory. Strangely, it was missing.Gravatar ppedrot2013-07-24
* Change Hint Resolve, Immediate to take a global reference as argumentGravatar msozeau2012-10-26
* Updating headers.Gravatar herbelin2012-08-08
* isolate instances about Permutation and PermutationA which may slow rewriteGravatar letouzey2012-07-10
* Kills the useless tactic annotations "in |- *"Gravatar letouzey2012-07-05
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* list_eq_dec now transparent (wish #2786)Gravatar letouzey2012-06-01
* SetoidList: explicit the fact that InfA_compat won't use ltA_strorderGravatar letouzey2012-05-22
* List + Permutation : more results about nth_error and nthGravatar letouzey2012-05-18
* A notion of permutation for lists modulo a setoid equalityGravatar letouzey2012-05-02
* Uniformisation in the documentation: remove the use of 'coinductive' inGravatar aspiwack2012-04-13
* theories/, plugins/ and test-suite/ ported to the Arguments vernacularGravatar gareuselesinge2011-11-21
* Bug 2589: Documentation patch of Hendrik TewsGravatar pboutill2011-09-02
* A module out of Program to have list notations (bug 2463)Gravatar pboutill2011-04-08
* Simplify proofs in Permutation using generalized rewriting.Gravatar msozeau2011-03-04
* Remove obsolete TheoryListGravatar glondu2011-02-10
* Cosmetic : let's take advantage of the n-ary exists notationGravatar letouzey2010-12-17
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Made notations for exists, exists! and notations of Utf8.v recursive notationsGravatar herbelin2010-07-22
* 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
* Fixing definition of set_map (bug report #2111) which was actually alreadyGravatar herbelin2010-06-13