Skip to content

Commit

Permalink
Adapt to coq/coq#19370
Browse files Browse the repository at this point in the history
  • Loading branch information
proux01 committed Oct 7, 2024
1 parent 652a8cc commit 9f32ab2
Show file tree
Hide file tree
Showing 3 changed files with 3 additions and 3 deletions.
2 changes: 1 addition & 1 deletion serapi/serapi_protocol.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion sertop/comp_common.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion sertop/sertop_sexp.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down

0 comments on commit 9f32ab2

Please sign in to comment.