diff options
| author | Emilio Jesus Gallego Arias | 2020-02-01 02:19:01 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-02-12 19:17:58 +0100 |
| commit | f12f88750ace921e01bbfd12758bd57410311e60 (patch) | |
| tree | f3ac223522d0a332c0ca0f4f073e35c2f8bed549 /plugins/syntax/string_notation.ml | |
| parent | 03118b16a5fb30d4172b613b4cbfb5c82c0c7552 (diff) | |
[toplevel] Make toplevel loop tail-recursive again
In previous refactorings `vernac_loop` stopped being tail-recursive,
we refactor code a bit and make it back into tail-recursive form.
Diffstat (limited to 'plugins/syntax/string_notation.ml')
0 files changed, 0 insertions, 0 deletions