diff options
| author | Gabriel Scherer | 2021-01-08 18:48:42 +0100 |
|---|---|---|
| committer | Gabriel Scherer | 2021-01-28 16:31:55 +0100 |
| commit | 32dee1c6fe4bf52e5065783ca6b693b74295ebde (patch) | |
| tree | f2043cf949c3a8eefb14016cc2fcf1f0b1b298e9 /pretyping | |
| parent | a54a5b83becd3ef7feef1352b56d10a3d74be85f (diff) | |
vernac/declaremods: make object collection tail-recursive
This patch is trying to upstream a jsCoq patch that was written to
solve Stack Overflow issues:
https://github.com/jscoq/jscoq/blob/v8.12/etc/patches/cps.patch
It turns List.fold_right in vernac/declaremods into List.fold_left
on a reversed lit.
Diffstat (limited to 'pretyping')
0 files changed, 0 insertions, 0 deletions