aboutsummaryrefslogtreecommitdiff
path: root/theories/Lists/List.v
AgeCommit message (Expand)Author
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-03-14Fix 3 unused-intro-pattern warnings in stdlib.Théo Zimmermann
2016-10-24Remove v62 from stdlib.Théo Zimmermann
2016-09-29Move vector/list compat notations to their relevant filesJason Gross
2016-09-26Remove spaces from around list notationsJason Gross
2016-06-18Giving a more natural semantics to injection by default.Hugo Herbelin
2016-04-27Revert "Temporary hack to compensate missing comma while re-printing tactic"Hugo Herbelin
2016-04-27Temporary hack to compensate missing comma while re-printing tacticHugo Herbelin
2016-02-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-02-19Fixing bug #4582: cannot override notation [ x ].Pierre-Marie Pédrot
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-12-17Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-15Proof using: do not clear unused section hyps automaticallyEnrico Tassi
2015-10-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-14Fix some typos.Guillaume Melquiond
2015-10-13Fix some typos.Guillaume Melquiond
2015-05-15Merge v8.5 into trunkHugo Herbelin
2015-05-12List.nth_error directly produces Some/None instead of value/errorPierre Letouzey
2015-05-05Merge branch 'v8.5'Pierre-Marie Pédrot
2015-05-01Giving to "subst" a more natural semantic (fixing #4214) by using allHugo Herbelin
2015-04-09Merge branch 'v8.5' into trunkPierre Letouzey
2015-04-09Prove [map_ext] using [map_ext_in].Nickolai Zeldovich
2015-04-09Add a [map_ext_in] lemma to List.v.Nickolai Zeldovich
2015-01-16Add two lemmas about firstn to the List standard library.Sébastien Hinderer
2015-01-16Lemmas related to the firstn function over lists.Sébastien Hinderer
2015-01-12Update headers.Maxime Dénès
2014-12-28Use [Proof using] to make sure that [List.in_flat_map] doesn't grab too many ...Arnaud Spiwack
2014-12-18Adds two lemmas about hderror to the List standard library.Sébastien Hinderer
2014-12-18Implement the nodup function on lists and prove associated results.Sébastien Hinderer
2014-12-18Lists: enhanced version of Seb's last commit on Exists/ForallPierre Letouzey
2014-12-18Lists: a few results on Exists and Forall and a bit of code cleanup.Sébastien Hinderer
2014-12-11List.v: sequel to Sebastien's commit (some cosmetics + a few shorter proofs)Pierre Letouzey
2014-12-11First series of results on lists.Sébastien Hinderer
2014-08-05Improving printing of "[]" (nil) in spite of the risk of collisionHugo Herbelin
2014-08-05Testing a replacement of "cut" by "enough" on a couple of test files.Hugo Herbelin
2014-05-06Try a new way of handling template universe levelsMatthieu Sozeau
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-02-07FinFun.v: results about injective/surjective/bijective fonctions over finite ...Pierre Letouzey
2013-12-20List: Bug 3039 weaker requirement for fold symmetricPierre Boutillier
2013-07-24Added a concat function to List theory. Strangely, it was missing.ppedrot
2012-08-08Updating headers.herbelin
2012-07-05ZArith + other : favor the use of modern names instead of compat notationsletouzey
2012-06-01list_eq_dec now transparent (wish #2786)letouzey
2012-05-18List + Permutation : more results about nth_error and nthletouzey
2011-09-02Bug 2589: Documentation patch of Hendrik Tewspboutill
2011-04-08A module out of Program to have list notations (bug 2463)pboutill
2010-12-17Cosmetic : let's take advantage of the n-ary exists notationletouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 16:58:21 +0000