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 | |
| 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')
| -rw-r--r-- | toplevel/coqloop.ml | 2 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 2 |
2 files changed, 2 insertions, 2 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 *) diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index c4c8492a4a..92e664d56b 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -110,7 +110,7 @@ let load_vernac_core ~echo ~check ~interactive ~state file = let state = Flags.silently (interp_vernac ~check ~interactive ~state) ast in - loop state (state.sid :: ids) + (loop [@ocaml.tailcall]) state (state.sid :: ids) in try loop state [] with any -> (* whatever the exception *) |