diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-10-11 22:53:56 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-10-17 20:14:13 +0200 |
| commit | 35961a4ff5a5b8c9b9786cbab0abd279263eb655 (patch) | |
| tree | cc6a7facef22a057d0cf364476f0299b71a4e54e /toplevel/coqloop.ml | |
| parent | 12f9dbf211b7ee27aecda09cf4209084ccaae5a6 (diff) | |
Vernac.ml: inlining read_vernac_file within load_vernac.
Also renaming vernac_com into interp_vernac and eval_expr into
process_vernac to clarify that it does side-effects (on the contrary
of Stm.interp/Vernacentries.interp).
Diffstat (limited to 'toplevel/coqloop.ml')
| -rw-r--r-- | toplevel/coqloop.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index ea7539fce..f0f8f1864 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -34,7 +34,7 @@ let resize_buffer ibuf = ibuf.str <- nstr (* Delete all irrelevant lines of the input buffer. Keep the last line - in the buffer (useful when there are several commands on the same line. *) + in the buffer (useful when there are several commands on the same line). *) let resynch_buffer ibuf = match ibuf.bols with @@ -299,7 +299,7 @@ let do_vernac () = resynch_buffer top_buffer; try let input = (top_buffer.tokens, None) in - Vernac.eval_expr top_buffer.tokens (read_sentence input) + Vernac.process_expr top_buffer.tokens (read_sentence input) with | End_of_input | CErrors.Quit -> top_stderr (fnl ()); raise CErrors.Quit |