diff --git a/serapi/serapi_protocol.ml b/serapi/serapi_protocol.ml index 29493fc0..0b340d1d 100644 --- a/serapi/serapi_protocol.ml +++ b/serapi/serapi_protocol.ml @@ -891,7 +891,7 @@ let exec_cmd (st : State.t) (cmd : cmd) : answer_kind list * State.t = coq_protect st @@ fun () -> match cmd with | NewDoc opts -> let stm_options = Stm.AsyncOpts.default_opts in - let require_libs = Option.default [{Coqargs.lib="Stdlib.Init.Prelude"; prefix=None; export=Some Lib.Export;}] opts.require_libs in + let require_libs = Option.default [{Coqargs.lib="Stdlib.Init.Prelude"; prefix=None; export=Some Lib.Export; allow_failure=false}] opts.require_libs in Stm.init_process stm_options; let ndoc = { Stm.doc_type = Stm.(Interactive opts.top_name) ; injections = List.map (fun x -> Coqargs.RequireInjection x) require_libs diff --git a/sertop/comp_common.ml b/sertop/comp_common.ml index a722446d..e9fb5707 100644 --- a/sertop/comp_common.ml +++ b/sertop/comp_common.ml @@ -79,7 +79,7 @@ let create_document ~debug ~set_impredicative_set ~disallow_sprop ~ml_path ~load else stm_options in - let injections = [Coqargs.RequireInjection {lib="Stdlib.Init.Prelude"; prefix=None; export=Some Lib.Import;}] in + let injections = [Coqargs.RequireInjection {lib="Stdlib.Init.Prelude"; prefix=None; export=Some Lib.Import; allow_failure=false}] in Stm.init_process stm_options; let ndoc = { Stm.doc_type = Stm.VoDoc in_file ; injections diff --git a/sertop/sertop_sexp.ml b/sertop/sertop_sexp.ml index 11546c37..fce501ba 100644 --- a/sertop/sertop_sexp.ml +++ b/sertop/sertop_sexp.ml @@ -234,7 +234,7 @@ let ser_loop ser_opts = let injections = if ser_opts.no_prelude then [] - else [Coqargs.RequireInjection {lib="Stdlib.Init.Prelude"; prefix=None; export=Some Lib.Import;}] in + else [Coqargs.RequireInjection {lib="Stdlib.Init.Prelude"; prefix=None; export=Some Lib.Import; allow_failure=false}] in let stm_options = Sertop_init.process_stm_flags ser_opts.async in Stm.init_process stm_options;