From 83c63a5075fb55e4e3291e163417bcffaf009dcd Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 21 Nov 2017 13:14:17 +0100 Subject: [stm] Allow delayed constant in interactive mode. This setting is a debug assertion, due to the many flags we still over-approximate setting the flag to true to all interactive environments. [So the assert is checked in vo compilation] Fixes #6152. --- stm/stm.ml | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index 864fff9e0..359890eb7 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2478,12 +2478,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 -- cgit v1.2.3