From 2da82387bb66c03b388bef1d16cf373511636f42 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Fri, 25 Oct 2024 13:28:35 +0200
Subject: [PATCH] Adapt to coq/coq#19757 (Coqargs is pure)

---
 serapi/serapi_protocol.ml   | 2 +-
 serlib_extra/ser_coqargs.ml | 4 ++++
 sertop/comp_common.ml       | 2 +-
 sertop/sertop_sexp.ml       | 4 ++--
 4 files changed, 8 insertions(+), 4 deletions(-)

diff --git a/serapi/serapi_protocol.ml b/serapi/serapi_protocol.ml
index f69bc610..a935d834 100644
--- a/serapi/serapi_protocol.ml
+++ b/serapi/serapi_protocol.ml
@@ -892,7 +892,7 @@ let exec_cmd (st : State.t) (cmd : cmd) : answer_kind list * State.t =
   | NewDoc opts   ->
     (* spawn_args probably wrong *)
     let stm_options = Stm.AsyncOpts.default_opts ~spawn_args:[] in
-    let require_libs = Option.default [{Coqargs.lib="Stdlib.Init.Prelude"; prefix=None; export=Some Lib.Export; allow_failure=false}] opts.require_libs in
+    let require_libs = Option.default [{Coqargs.lib="Stdlib.Init.Prelude"; prefix=None; export=Some 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/serlib_extra/ser_coqargs.ml b/serlib_extra/ser_coqargs.ml
index bebfadb7..f4e2b965 100644
--- a/serlib_extra/ser_coqargs.ml
+++ b/serlib_extra/ser_coqargs.ml
@@ -26,6 +26,10 @@ type top =
   [%import: Coqargs.top]
   [@@deriving sexp]
 
+type export_flag =
+  [%import: Coqargs.export_flag]
+  [@@deriving sexp]
+
 type require_injection =
   [%import: Coqargs.require_injection]
   [@@deriving sexp]
diff --git a/sertop/comp_common.ml b/sertop/comp_common.ml
index e9fb5707..81fffb3f 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; allow_failure=false}] in
+  let injections = [Coqargs.RequireInjection {lib="Stdlib.Init.Prelude"; prefix=None; export=Some 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 fce501ba..8c5fa0af 100644
--- a/sertop/sertop_sexp.ml
+++ b/sertop/sertop_sexp.ml
@@ -140,7 +140,7 @@ let out_answer opts =
 let doc_type topfile =
   match topfile with
   | None ->
-    let sertop_dp = Names.(DirPath.make [Id.of_string "SerTop"]) in
+    let sertop_dp = "SerTop" in
     Stm.Interactive (TopLogical sertop_dp)
   | Some filename -> Stm.Interactive (Coqargs.TopPhysical filename)
 
@@ -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; allow_failure=false}] in
+    else [Coqargs.RequireInjection {lib="Stdlib.Init.Prelude"; prefix=None; export=Some Import; allow_failure=false}] in
 
   let stm_options = Sertop_init.process_stm_flags ser_opts.async in
   Stm.init_process stm_options;