Merge pull request #426 from proux01/coq_19370

Adapt to coq/coq#19370
rocq-archive · Oct 11, 2024 · 5e8d6ad · 5e8d6ad
2 parents 652a8cc + 9f32ab2
commit 5e8d6ad
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 3 deletions.
diff --git 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
@@ -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
@@ -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;