aboutsummaryrefslogtreecommitdiff
path: root/theories/Lists
AgeCommit message (Expand)Author
2019-01-23Pass some files to strict focusing mode.Gaëtan Gilbert
2018-12-19Put #[universes(template)] on all auto template spots in stdlibGaëtan Gilbert
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-04-16Protecting against a "deprecated cofix" warning.Hugo Herbelin
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-06-01drop vo.itarget files and compute the corresponding the corresponding values ...Matej Kosik
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-08-05Merge branch 'v8.5'Pierre-Marie Pédrot
2015-07-31Remove some outdated files and fix permissions.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-03-04Introducing MMaps, a modernized FMaps.Pierre Letouzey
2015-03-04Introducing MMaps, a modernized FMaps.Pierre Letouzey
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-16ListSet: follow-up of Sebastien's last commitPierre Letouzey
2015-01-16Work in progress on listset.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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:15:04 +0000