index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
theories
/
Lists
Commit message (
Expand
)
Author
Age
*
Protecting against a "deprecated cofix" warning.
Hugo Herbelin
2018-04-16
*
Merge PR #6855: Update headers following #6543.
Maxime Dénès
2018-03-05
|
\
*
|
Remove VOld compatibility flag.
Théo Zimmermann
2018-03-02
|
*
Update headers following #6543.
Théo Zimmermann
2018-02-27
|
/
*
Make list functions returning sumbools transparent
Tej Chajed
2017-11-15
*
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
*
drop vo.itarget files and compute the corresponding the corresponding values ...
Matej Kosik
2017-06-01
*
Fix 3 unused-intro-pattern warnings in stdlib.
Théo Zimmermann
2017-03-14
*
Remove v62 from stdlib.
Théo Zimmermann
2016-10-24
*
Move vector/list compat notations to their relevant files
Jason Gross
2016-09-29
*
Remove spaces from around list notations
Jason Gross
2016-09-26
*
Giving a more natural semantics to injection by default.
Hugo Herbelin
2016-06-18
*
Revert "Temporary hack to compensate missing comma while re-printing tactic"
Hugo Herbelin
2016-04-27
*
Temporary hack to compensate missing comma while re-printing tactic
Hugo Herbelin
2016-04-27
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-02-21
|
\
|
*
Fixing bug #4582: cannot override notation [ x ].
Pierre-Marie Pédrot
2016-02-19
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
|
|
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-12-17
|
\
|
|
*
Proof using: do not clear unused section hyps automatically
Enrico Tassi
2015-12-15
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-15
|
\
|
|
*
Fix some typos.
Guillaume Melquiond
2015-10-14
|
*
Fix some typos.
Guillaume Melquiond
2015-10-13
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-08-05
|
\
|
|
*
Remove some outdated files and fix permissions.
Guillaume Melquiond
2015-07-31
*
|
Merge v8.5 into trunk
Hugo Herbelin
2015-05-15
|
\
|
|
*
List.nth_error directly produces Some/None instead of value/error
Pierre Letouzey
2015-05-12
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-05-05
|
\
|
|
*
Giving to "subst" a more natural semantic (fixing #4214) by using all
Hugo Herbelin
2015-05-01
*
|
Merge branch 'v8.5' into trunk
Pierre Letouzey
2015-04-09
|
\
|
|
*
Prove [map_ext] using [map_ext_in].
Nickolai Zeldovich
2015-04-09
|
*
Add a [map_ext_in] lemma to List.v.
Nickolai Zeldovich
2015-04-09
|
*
Introducing MMaps, a modernized FMaps.
Pierre Letouzey
2015-03-04
*
|
Introducing MMaps, a modernized FMaps.
Pierre Letouzey
2015-03-04
*
|
Add two lemmas about firstn to the List standard library.
Sébastien Hinderer
2015-01-16
*
|
Lemmas related to the firstn function over lists.
Sébastien Hinderer
2015-01-16
*
|
ListSet: follow-up of Sebastien's last commit
Pierre Letouzey
2015-01-16
*
|
Work in progress on listset.
Sébastien Hinderer
2015-01-16
|
/
*
Update headers.
Maxime Dénès
2015-01-12
*
Use [Proof using] to make sure that [List.in_flat_map] doesn't grab too many ...
Arnaud Spiwack
2014-12-28
*
Adds two lemmas about hderror to the List standard library.
Sébastien Hinderer
2014-12-18
*
Implement the nodup function on lists and prove associated results.
Sébastien Hinderer
2014-12-18
*
Lists: enhanced version of Seb's last commit on Exists/Forall
Pierre Letouzey
2014-12-18
*
Lists: a few results on Exists and Forall and a bit of code cleanup.
Sébastien Hinderer
2014-12-18
*
List.v: sequel to Sebastien's commit (some cosmetics + a few shorter proofs)
Pierre Letouzey
2014-12-11
*
First series of results on lists.
Sébastien Hinderer
2014-12-11
*
Clarifying the role of ListSet.v in the library, compared to other
Hugo Herbelin
2014-11-18
*
Improving printing of "[]" (nil) in spite of the risk of collision
Hugo Herbelin
2014-08-05
*
Testing a replacement of "cut" by "enough" on a couple of test files.
Hugo Herbelin
2014-08-05
*
More proofs independent of the names generated by induction/elim over
Hugo Herbelin
2014-08-05
[next]