aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Lists
Commit message (Expand)AuthorAge
* Fix 3 unused-intro-pattern warnings in stdlib.Gravatar Théo Zimmermann2017-03-14
* Remove v62 from stdlib.Gravatar Théo Zimmermann2016-10-24
* Move vector/list compat notations to their relevant filesGravatar Jason Gross2016-09-29
* Remove spaces from around list notationsGravatar Jason Gross2016-09-26
* Giving a more natural semantics to injection by default.Gravatar Hugo Herbelin2016-06-18
* Revert "Temporary hack to compensate missing comma while re-printing tactic"Gravatar Hugo Herbelin2016-04-27
* Temporary hack to compensate missing comma while re-printing tacticGravatar Hugo Herbelin2016-04-27
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-02-21
|\
| * Fixing bug #4582: cannot override notation [ x ].Gravatar Pierre-Marie Pédrot2016-02-19
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-17
|\|
| * Proof using: do not clear unused section hyps automaticallyGravatar Enrico Tassi2015-12-15
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-15
|\|
| * Fix some typos.Gravatar Guillaume Melquiond2015-10-14
| * Fix some typos.Gravatar Guillaume Melquiond2015-10-13
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-08-05
|\|
| * Remove some outdated files and fix permissions.Gravatar Guillaume Melquiond2015-07-31
* | Merge v8.5 into trunkGravatar Hugo Herbelin2015-05-15
|\|
| * List.nth_error directly produces Some/None instead of value/errorGravatar Pierre Letouzey2015-05-12
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-05-05
|\|
| * Giving to "subst" a more natural semantic (fixing #4214) by using allGravatar Hugo Herbelin2015-05-01
* | Merge branch 'v8.5' into trunkGravatar Pierre Letouzey2015-04-09
|\|
| * 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
* | Introducing MMaps, a modernized FMaps.Gravatar Pierre Letouzey2015-03-04
* | Add two lemmas about firstn to the List standard library.Gravatar Sébastien Hinderer2015-01-16
* | Lemmas related to the firstn function over lists.Gravatar Sébastien Hinderer2015-01-16
* | ListSet: follow-up of Sebastien's last commitGravatar Pierre Letouzey2015-01-16
* | Work in progress on listset.Gravatar Sébastien Hinderer2015-01-16
|/
* 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