diff options
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 *) |