diff options
| author | Gaëtan Gilbert | 2019-02-08 13:34:02 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-02-08 13:34:02 +0100 |
| commit | 6c06f36b2dd1812454d40cbde1da28e1ea8be67e (patch) | |
| tree | 62782d00b4c5781caf89dfc08e804f220e6cc790 /stm/stm.mli | |
| parent | 99c1d7b0ae1beed66fe8dd6a06db84dc0c8322d8 (diff) | |
Make boot flag into a normal option (no global flag).
Diffstat (limited to 'stm/stm.mli')
| -rw-r--r-- | stm/stm.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/stm/stm.mli b/stm/stm.mli index 821ab59a43..313ac58111 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -67,6 +67,10 @@ type stm_init_options = { some point. *) doc_type : stm_doc_type; + (* Allow compiling modules in the Coq prefix. Irrelevant in + interactive mode. *) + allow_coq_overwrite : bool; + (* Initial load path in scope for the document. Usually extracted from -R options / _CoqProject *) iload_path : Mltop.coq_path list; |
