aboutsummaryrefslogtreecommitdiff
path: root/stm/stm.mli
diff options
context:
space:
mode:
authorGaëtan Gilbert2019-02-08 13:34:02 +0100
committerGaëtan Gilbert2019-02-08 13:34:02 +0100
commit6c06f36b2dd1812454d40cbde1da28e1ea8be67e (patch)
tree62782d00b4c5781caf89dfc08e804f220e6cc790 /stm/stm.mli
parent99c1d7b0ae1beed66fe8dd6a06db84dc0c8322d8 (diff)
Make boot flag into a normal option (no global flag).
Diffstat (limited to 'stm/stm.mli')
-rw-r--r--stm/stm.mli4
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;