diff options
| author | Emilio Jesus Gallego Arias | 2019-08-24 02:36:52 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-10-07 10:36:37 +0200 |
| commit | ebe43dddd50b96c8553e1fbdf3d26413eac47806 (patch) | |
| tree | 4f8a2a459fb90f68c434d75ae032bd797c7c6756 /toplevel | |
| parent | ef7cade43d514cb8f3d6022c298fdc467fcc4a33 (diff) | |
[vernac] Split vernacular translation and interpretation.
This allows UI clients to implement a different state management
strategy with regards to proofs, and in particular to override
`Vernacinterp.interp`.
This is work in progress towards having a true `VtTactic` which shall
not perform any state changes non-functionally, and actually removing
the series of `assert false` due to meta-vernacs.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqargs.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 113b1fb5d7..c85b656171 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -497,7 +497,7 @@ let parse_args ~help ~init arglist : t * string list = { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with Stm.AsyncOpts.async_proofs_never_reopen_branch = true }}} - |"-test-mode" -> Vernacentries.test_mode := true; oval + |"-test-mode" -> Vernacinterp.test_mode := true; oval |"-beautify" -> Flags.beautify := true; oval |"-bt" -> Backtrace.record_backtrace true; oval |"-color" -> set_color oval (next ()) |