diff options
| author | Emilio Jesus Gallego Arias | 2020-06-13 17:56:50 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-06-13 17:57:37 +0200 |
| commit | ce26ccfd0160265af975f84727e45bb97da39628 (patch) | |
| tree | 357c800f63cef410d480bb4d1c72f3066afe0e90 /toplevel/coqloop.ml | |
| parent | 13e8d04b2f080fbc7ca169bc39e53c8dd091d279 (diff) | |
[toplevel] Annotate tailcall functions
This will ensure that we don't introduce problems as it has happened
in the past.
While we are at it, we fix one easy case of non-tail call.
Diffstat (limited to 'toplevel/coqloop.ml')
| -rw-r--r-- | toplevel/coqloop.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 2c5faa4df7..79de3c86b6 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -499,7 +499,7 @@ let rec vernac_loop ~state = if !print_emacs then top_stderr (str (top_buffer.prompt state.doc)); resynch_buffer top_buffer; let state, drop = read_and_execute ~state in - if drop then state else vernac_loop ~state + if drop then state else (vernac_loop [@ocaml.tailcall]) ~state (* Default toplevel loop, machinery for drop is below *) |