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 /interp | |
| 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 'interp')
0 files changed, 0 insertions, 0 deletions