aboutsummaryrefslogtreecommitdiff
path: root/theories/Lists/List.v
AgeCommit message (Expand)Author
2019-05-25Modifying theories to preferably use the "[= ]" syntax, and,Hugo Herbelin
2019-02-28Implement a method for manual declaration of implicits.Jasper Hugunin
2018-11-27Added two proofs to the Lists library. The first, Forall_inv_tail, extends Fo...llee454@gmail.com
2018-11-14Deprecate hint declaration/removal with no specified databaseMaxime Dénès
2018-09-29New lemmas for List.vSimon Marechal
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-03-02Remove VOld compatibility flag.Théo Zimmermann
2018-02-27Update headers following #6543.Théo Zimmermann
2017-11-15Make list functions returning sumbools transparentTej Chajed
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 16:12:55 +0000