diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-11-27 16:55:05 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-11-27 16:55:05 +0100 |
| commit | 68061d8d464d0c62442675897c9c5f6db8d2b2e4 (patch) | |
| tree | d0b0b312054b505a5bd5d1c9da71de70f9cc2f93 /stm/stm.ml | |
| parent | 2fcbfcfe8066bcf7ee40830bb9043b0cfd754e63 (diff) | |
| parent | 83c63a5075fb55e4e3291e163417bcffaf009dcd (diff) | |
Merge PR #6207: [stm] Allow delayed constant in interactive mode.
Diffstat (limited to 'stm/stm.ml')
| -rw-r--r-- | stm/stm.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 12f414f39..0ee9ea084 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2483,12 +2483,16 @@ let new_doc { doc_type ; require_libs } = begin match doc_type with | Interactive ln -> + Safe_typing.allow_delayed_constants := true; Declaremods.start_library ln + | VoDoc ln -> let ldir = Flags.verbosely Library.start_library ln in VCS.set_ldir ldir; set_compilation_hints ln + | VioDoc ln -> + Safe_typing.allow_delayed_constants := true; let ldir = Flags.verbosely Library.start_library ln in VCS.set_ldir ldir; set_compilation_hints ln |