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/vernac.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/vernac.ml')
| -rw-r--r-- | toplevel/vernac.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 *) |