Merge PR #12097: Interleave commandline require/set/unset commands

Ack-by: Zimmi48
Reviewed-by: ejgallego

13 files changed, 170 insertions, 111 deletions

diff --git a/doc/changelog/08-tools/11851-coqc-flags-fix.rst b/doc/changelog/08-tools/11851-coqc-flags-fix.rst
index a07e48d2d8..ff736641b4 100644
--- a/doc/changelog/08-tools/11851-coqc-flags-fix.rst
+++ b/doc/changelog/08-tools/11851-coqc-flags-fix.rst
@@ -1,6 +1,9 @@
 - **Changed:**
-  The order in which the require/load flags `-l`, `-ri`, `-re`, `-rfrom`, etc.
-  and the option set flags `-set`, `-unset` are processed have been reversed.
-  In the new behavior, require/load flags are processed before option flags.
-  (`#11851 <https://github.com/coq/coq/pull/11851>`_,
+  The order in which the require flags `-ri`, `-re`, `-rfrom`, etc.
+  and the option flags `-set`, `-unset` are given now matters.  In
+  particular, it is now possible to interleave the loading of plugins
+  and the setting of options by choosing the right order for these
+  flags.  The load flags `-l` and `-lv` are still processed afterward
+  for now (`#11851 <https://github.com/coq/coq/pull/11851>`_ and
+  `#12097 <https://github.com/coq/coq/pull/12097>`_,
   by Lasse Blaauwbroek).
diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst
index 58fd49c390..d4ceffac9f 100644
--- a/doc/sphinx/practical-tools/coq-commands.rst
+++ b/doc/sphinx/practical-tools/coq-commands.rst
@@ -151,7 +151,7 @@ and ``coqtop``, unless stated otherwise:
   while processing options such as -R and -Q. By default, only the
   conventional version control management directories named CVS
   and_darcs are excluded.
-:-nois: Start from an empty state instead of loading the Init.Prelude
+:-nois, -noinit: Start from an empty state instead of loading the `Init.Prelude`
   module.
 :-init-file *file*: Load *file* as the resource file instead of
   loading the default resource file from the standard configuration
@@ -163,26 +163,53 @@ and ``coqtop``, unless stated otherwise:
   |Coq| script from *file.v*. Write its contents to the standard output as
   it is executed.
 :-load-vernac-object *qualid*: Load |Coq| compiled library :n:`@qualid`. This
-  is equivalent to running :cmd:`Require` :n:`qualid`.
+  is equivalent to running :cmd:`Require` :n:`@qualid`.
+
+  .. _interleave-command-line:
+
+  .. note::
+
+     Note that the relative order of this command-line option and its
+     variants (`-rfrom`, `-ri`, `-re`, etc.)  and of the `-set` and
+     `-unset` options matters since the various :cmd:`Require`,
+     :cmd:`Require Import`, :cmd:`Require Export`, :cmd:`Set` and
+     :cmd:`Unset` commands will be executed in the order specified on
+     the command-line.
+
 :-rfrom *dirpath* *qualid*: Load |Coq| compiled library :n:`@qualid`.
-  This is equivalent to running :n:`From` :n:`@dirpath` :cmd:`Require Import` :n:`@qualid`.
+  This is equivalent to running :cmd:`From <From ... Require>`
+  :n:`@dirpath` :cmd:`Require <From ... Require>` :n:`@qualid`.
+  See the :ref:`note above <interleave-command-line>` regarding the order
+  of command-line options.
 :-ri *qualid*, -require-import *qualid*: Load |Coq| compiled library :n:`@qualid` and import it.
   This is equivalent to running :cmd:`Require Import` :n:`@qualid`.
+  See the :ref:`note above <interleave-command-line>` regarding the order
+  of command-line options.
 :-re *qualid*, -require-export *qualid*: Load |Coq| compiled library :n:`@qualid` and transitively import it.
   This is equivalent to running :cmd:`Require Export` :n:`@qualid`.
-:-rifrom *dirpath* *qualid*, -require-import-from *dirpath* *qualid*: Load |Coq| compiled library :n:`@qualid` and import it.
-  This is equivalent to running :n:`From` :n:`@dirpath` :cmd:`Require Import` :n:`@qualid`.
-:-refrom *dirpath* *qualid*, -require-export-from *dirpath* *qualid*: Load |Coq| compiled library :n:`@qualid` and transitively import it.
-  This is equivalent to running :n:`From` :n:`@dirpath` :cmd:`Require Export` :n:`@qualid`.
+  See the :ref:`note above <interleave-command-line>` regarding the order
+  of command-line options.
+:-rifrom *dirpath* *qualid*, -require-import-from *dirpath* *qualid*:
+  Load |Coq| compiled library :n:`@qualid` and import it.  This is
+  equivalent to running :cmd:`From <From ... Require>` :n:`@dirpath`
+  :cmd:`Require Import <From ... Require>` :n:`@qualid`.  See the
+  :ref:`note above <interleave-command-line>` regarding the order of
+  command-line options.
+:-refrom *dirpath* *qualid*, -require-export-from *dirpath* *qualid*:
+  Load |Coq| compiled library :n:`@qualid` and transitively import it.
+  This is equivalent to running :cmd:`From <From ... Require>`
+  :n:`@dirpath` :cmd:`Require Export <From ... Require>` :n:`@qualid`.
+  See the :ref:`note above <interleave-command-line>` regarding the
+  order of command-line options.
 :-batch: Exit just after argument parsing. Available for ``coqtop`` only.
 :-verbose: Output the content of the input file as it is compiled.
   This option is available for ``coqc`` only.
 :-vos: Indicate |Coq| to skip the processing of opaque proofs
-  (i.e., proofs ending with ``Qed`` or ``Admitted``), output a ``.vos`` files
+  (i.e., proofs ending with :cmd:`Qed` or :cmd:`Admitted`), output a ``.vos`` files
   instead of a ``.vo`` file, and to load ``.vos`` files instead of ``.vo`` files
-  when interpreting ``Require`` commands.
+  when interpreting :cmd:`Require` commands.
 :-vok: Indicate |Coq| to check a file completely, to load ``.vos`` files instead
-  of ``.vo`` files when interpreting ``Require`` commands, and to output an empty
+  of ``.vo`` files when interpreting :cmd:`Require` commands, and to output an empty
   ``.vok`` files upon success instead of writing a ``.vo`` file.
 :-w (all|none|w₁,…,wₙ): Configure the display of warnings. This
   option expects all, none or a comma-separated list of warning names or
@@ -192,7 +219,7 @@ and ``coqtop``, unless stated otherwise:
   the output channel supports ANSI escape sequences.
 :-diffs (on|off|removed): *Coqtop only*.  Controls highlighting of differences
   between proof steps.  ``on`` highlights added tokens, ``removed`` highlights both added and
-  removed tokens.  Requires that ``–color`` is enabled.  (see Section
+  removed tokens.  Requires that ``-color`` is enabled.  (see Section
   :ref:`showing_diffs`).
 :-beautify: Pretty-print each command to *file.beautified* when
   compiling *file.v*, in order to get old-fashioned
@@ -218,17 +245,25 @@ and ``coqtop``, unless stated otherwise:
   changes in the auto-generated name scheme. The options are provided to
   facilitate tracking down problems.
 :-set *string*: Enable flags and set options. *string* should be
-   ``Option Name=value``, the value is interpreted according to the
-   type of the option. For flags ``Option Name`` is equivalent to
-   ``Option Name=true``. For instance ``-set "Universe Polymorphism"``
+   :n:`@setting_name=value`, the value is interpreted according to the
+   type of the option. For flags :n:`@setting_name` is equivalent to
+   :n:`@setting_name=true`. For instance ``-set "Universe Polymorphism"``
    will enable :flag:`Universe Polymorphism`. Note that the quotes are
-   shell syntax, Coq does not see them. Flags are processed after initialization
-   of the document. This includes the `Prelude` if loaded and any libraries loaded
-   through the `-l`, `-lv`, `-r`, `-re`, `-ri`, `rfrom`, `-refrom` and `-rifrom`
-   options.
+   shell syntax, Coq does not see them.
+   See the :ref:`note above <interleave-command-line>` regarding the order
+   of command-line options.
 :-unset *string*: As ``-set`` but used to disable options and flags.
-:-compat *version*: Attempt to maintain some backward-compatibility
-  with a previous version.
+  *string* must be :n:`"@setting_name"`.
+  See the :ref:`note above <interleave-command-line>` regarding the order
+  of command-line options.
+:-compat *version*: Load a file that sets a few options to maintain
+  partial backward-compatibility with a previous version.  This is
+  equivalent to :cmd:`Require Import` `Coq.Compat.CoqXXX` with `XXX`
+  one of the last three released versions (including the current
+  version).  Note that the :ref:`explanations above
+  <interleave-command-line>` regarding the order of command-line
+  options apply, and this could be relevant if you are resetting some
+  of the compatibility options.
 :-dump-glob *file*: Dump references for global names in file *file*
   (to be used by coqdoc, see :ref:`coqdoc`). By default, if *file.v* is being
   compiled, *file.glob* is used.
diff --git a/stm/stm.ml b/stm/stm.ml
index 5790bfc07e..b296f8f08f 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2576,6 +2576,21 @@ end (* }}} *)
 (******************************************************************************)
 
 (** STM initialization options: *)
+
+type option_command = OptionSet of string option | OptionUnset
+
+type injection_command =
+  | OptionInjection of (Goptions.option_name * option_command)
+  (** Set flags or options before the initial state is ready. *)
+  | RequireInjection of (string * string option * bool option)
+  (** Require libraries before the initial state is
+     ready. Parameters follow [Library], that is to say,
+     [lib,prefix,import_export] means require library [lib] from
+     optional [prefix] and [import_export] if [Some false/Some true]
+     is used.  *)
+  (* -load-vernac-source interleaving is not supported yet *)
+  (* | LoadInjection of (string * bool) *)
+
 type stm_init_options =
   { doc_type : stm_doc_type
   (** The STM does set some internal flags differently depending on
@@ -2589,12 +2604,9 @@ type stm_init_options =
   (** [vo] load paths for the document. Usually extracted from -R
      options / _CoqProject *)
 
-  ; require_libs : (string * string option * bool option) list
-  (** Require [require_libs] before the initial state is
-     ready. Parameters follow [Library], that is to say,
-     [lib,prefix,import_export] means require library [lib] from
-     optional [prefix] and [import_export] if [Some false/Some true]
-     is used.  *)
+  ; injections : injection_command list
+  (** Injects Require and Set/Unset commands before the initial
+     state is ready *)
 
   ; stm_options  : AsyncOpts.stm_opt
   (** Low-level STM options *)
@@ -2625,13 +2637,51 @@ let dirpath_of_file f =
   let ldir = Libnames.add_dirpath_suffix ldir0 id in
   ldir
 
-let new_doc { doc_type ; ml_load_path; vo_load_path; require_libs; stm_options } =
+let new_doc { doc_type ; ml_load_path; vo_load_path; injections; stm_options } =
 
   let require_file (dir, from, exp) =
     let mp = Libnames.qualid_of_string dir in
     let mfrom = Option.map Libnames.qualid_of_string from in
     Flags.silently (Vernacentries.vernac_require mfrom exp) [mp] in
 
+  let interp_set_option opt v old =
+    let open Goptions in
+    let err expect =
+      let opt = String.concat " " opt in
+      let got = v in (* avoid colliding with Pp.v *)
+      CErrors.user_err
+        Pp.(str "-set: " ++ str opt ++
+            str" expects " ++ str expect ++
+            str" but got " ++ str got)
+    in
+    match old with
+    | BoolValue _ ->
+      let v = match String.trim v with
+        | "true" -> true
+        | "false" | "" -> false
+        | _ -> err "a boolean"
+      in
+      BoolValue v
+    | IntValue _ ->
+      let v = String.trim v in
+      let v = match int_of_string_opt v with
+        | Some _ as v -> v
+        | None -> if v = "" then None else err "an int"
+      in
+      IntValue v
+    | StringValue _ -> StringValue v
+    | StringOptValue _ -> StringOptValue (Some v) in
+
+  let set_option = let open Goptions in function
+      | opt, OptionUnset -> unset_option_value_gen ~locality:OptLocal opt
+      | opt, OptionSet None -> set_bool_option_value_gen ~locality:OptLocal opt true
+      | opt, OptionSet (Some v) -> set_option_value ~locality:OptLocal (interp_set_option opt) opt v in
+
+  let handle_injection = function
+    | RequireInjection r -> require_file r
+    (* | LoadInjection l -> *)
+    | OptionInjection o -> set_option o in
+
   (* Set the options from the new documents *)
   AsyncOpts.cur_opt := stm_options;
 
@@ -2670,7 +2720,7 @@ let new_doc { doc_type ; ml_load_path; vo_load_path; require_libs; stm_options }
   end;
 
   (* Import initial libraries. *)
-  List.iter require_file require_libs;
+  List.iter handle_injection injections;
 
   (* We record the state at this point! *)
   State.define ~doc ~cache:true ~redefine:true (fun () -> ()) Stateid.initial;
diff --git a/stm/stm.mli b/stm/stm.mli
index 2c27d63b82..9780c96512 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -52,6 +52,20 @@ type stm_doc_type =
   | VioDoc      of string       (* file path *)
   | Interactive of interactive_top    (* module path *)
 
+type option_command = OptionSet of string option | OptionUnset
+
+type injection_command =
+  | OptionInjection of (Goptions.option_name * option_command)
+  (** Set flags or options before the initial state is ready. *)
+  | RequireInjection of (string * string option * bool option)
+  (** Require libraries before the initial state is
+     ready. Parameters follow [Library], that is to say,
+     [lib,prefix,import_export] means require library [lib] from
+     optional [prefix] and [import_export] if [Some false/Some true]
+     is used.  *)
+  (* -load-vernac-source interleaving is not supported yet *)
+  (* | LoadInjection of (string * bool) *)
+
 (** STM initialization options: *)
 type stm_init_options =
   { doc_type : stm_doc_type
@@ -66,12 +80,9 @@ type stm_init_options =
   (** [vo] load paths for the document. Usually extracted from -R
      options / _CoqProject *)
 
-  ; require_libs : (string * string option * bool option) list
-  (** Require [require_libs] before the initial state is
-     ready. Parameters follow [Library], that is to say,
-     [lib,prefix,import_export] means require library [lib] from
-     optional [prefix] and [import_export] if [Some false/Some true]
-     is used.  *)
+  ; injections : injection_command list
+  (** Injects Require and Set/Unset commands before the initial
+     state is ready *)
 
   ; stm_options  : AsyncOpts.stm_opt
   (** Low-level STM options *)
diff --git a/test-suite/output/interleave_options_bad_order.out b/test-suite/output/interleave_options_bad_order.out
new file mode 100644
index 0000000000..68dbaeb7b3
--- /dev/null
+++ b/test-suite/output/interleave_options_bad_order.out
@@ -0,0 +1,4 @@
+While loading initial state:
+Warning: There is no flag or option with this name: "Extraction Optimize".
+[unknown-option,option]
+Extraction Optimize is on
diff --git a/test-suite/output/interleave_options_bad_order.v b/test-suite/output/interleave_options_bad_order.v
new file mode 100644
index 0000000000..9a70674b02
--- /dev/null
+++ b/test-suite/output/interleave_options_bad_order.v
@@ -0,0 +1,3 @@
+(* coq-prog-args: ("-unset" "Extraction Optimize" "-ri" "Extraction") *)
+
+Test Extraction Optimize.
diff --git a/test-suite/output/interleave_options_correct_order.out b/test-suite/output/interleave_options_correct_order.out
new file mode 100644
index 0000000000..76bb2016eb
--- /dev/null
+++ b/test-suite/output/interleave_options_correct_order.out
@@ -0,0 +1 @@
+Extraction Optimize is off
diff --git a/test-suite/output/interleave_options_correct_order.v b/test-suite/output/interleave_options_correct_order.v
new file mode 100644
index 0000000000..7622d6ff52
--- /dev/null
+++ b/test-suite/output/interleave_options_correct_order.v
@@ -0,0 +1,3 @@
+(* coq-prog-args: ("-ri" "Extraction" "-unset" "Extraction Optimize") *)
+
+Test Extraction Optimize.
diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml
index c8b8660b92..524f818523 100644
--- a/toplevel/ccompile.ml
+++ b/toplevel/ccompile.ml
@@ -92,41 +92,6 @@ let create_empty_file filename =
   let f = open_out filename in
   close_out f
 
-let interp_set_option opt v old =
-  let open Goptions in
-  let err expect =
-    let opt = String.concat " " opt in
-    let got = v in (* avoid colliding with Pp.v *)
-    CErrors.user_err
-      Pp.(str "-set: " ++ str opt ++
-          str" expects " ++ str expect ++
-          str" but got " ++ str got)
-  in
-  match old with
-  | BoolValue _ ->
-    let v = match String.trim v with
-      | "true" -> true
-      | "false" | "" -> false
-      | _ -> err "a boolean"
-    in
-    BoolValue v
-  | IntValue _ ->
-    let v = String.trim v in
-    let v = match int_of_string_opt v with
-      | Some _ as v -> v
-      | None -> if v = "" then None else err "an int"
-    in
-    IntValue v
-  | StringValue _ -> StringValue v
-  | StringOptValue _ -> StringOptValue (Some v)
-
-let set_option = let open Goptions in function
-  | opt, OptionUnset -> unset_option_value_gen ~locality:OptLocal opt
-  | opt, OptionSet None -> set_bool_option_value_gen ~locality:OptLocal opt true
-  | opt, OptionSet (Some v) -> set_option_value ~locality:OptLocal (interp_set_option opt) opt v
-
-let set_options = List.iter set_option
-
 (* Compile a vernac file *)
 let compile opts copts ~echo ~f_in ~f_out =
   let open Vernac.State in
@@ -140,7 +105,7 @@ let compile opts copts ~echo ~f_in ~f_out =
                     ++ str ".")
   in
   let ml_load_path, vo_load_path = build_load_path opts in
-  let require_libs = require_libs opts in
+  let injections = injection_commands opts in
   let stm_options = opts.config.stm_flags in
   let output_native_objects = match opts.config.native_compiler with
     | NativeOff -> false | NativeOn {ondemand} -> not ondemand
@@ -165,11 +130,10 @@ let compile opts copts ~echo ~f_in ~f_out =
       let doc, sid = Topfmt.(in_phase ~phase:LoadingPrelude)
           Stm.new_doc
           Stm.{ doc_type = VoDoc long_f_dot_out; ml_load_path;
-                vo_load_path; require_libs; stm_options;
+                vo_load_path; injections; stm_options;
               } in
       let state = { doc; sid; proof = None; time = opts.config.time } in
       let state = load_init_vernaculars opts ~state in
-      set_options opts.config.set_options;
       let ldir = Stm.get_ldir ~doc:state.doc in
       Aux_file.(start_aux_file
         ~aux_file:(aux_file_name_for long_f_dot_out)
@@ -218,12 +182,11 @@ let compile opts copts ~echo ~f_in ~f_out =
       let doc, sid = Topfmt.(in_phase ~phase:LoadingPrelude)
           Stm.new_doc
           Stm.{ doc_type = VioDoc long_f_dot_out; ml_load_path;
-                vo_load_path; require_libs; stm_options;
+                vo_load_path; injections; stm_options;
               } in
 
       let state = { doc; sid; proof = None; time = opts.config.time } in
       let state = load_init_vernaculars opts ~state in
-      set_options opts.config.set_options;
       let ldir = Stm.get_ldir ~doc:state.doc in
       let state = Vernac.load_vernac ~echo ~check:false ~interactive:false ~state long_f_dot_in in
       let doc = Stm.finish ~doc:state.doc in
diff --git a/toplevel/ccompile.mli b/toplevel/ccompile.mli
index eb66dbaafc..8c154488d0 100644
--- a/toplevel/ccompile.mli
+++ b/toplevel/ccompile.mli
@@ -17,5 +17,3 @@ val compile_files : Coqargs.t -> Coqcargs.t -> unit
 
 (** [do_vio opts] process [.vio] files in [opts] *)
 val do_vio : Coqargs.t -> Coqcargs.t -> unit
-
-val set_options : (Goptions.option_name * Coqargs.option_command) list -> unit
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 17435c051e..c7ad5edb1f 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -38,8 +38,6 @@ type color = [`ON | `AUTO | `EMACS | `OFF]
 
 type native_compiler = NativeOff | NativeOn of { ondemand : bool }
 
-type option_command = OptionSet of string option | OptionUnset
-
 type coqargs_logic_config = {
   impredicative_set : Declarations.set_predicativity;
   indices_matter    : bool;
@@ -59,7 +57,6 @@ type coqargs_config = {
   debug       : bool;
   time        : bool;
   print_emacs : bool;
-  set_options : (Goptions.option_name * option_command) list;
 }
 
 type coqargs_pre = {
@@ -69,10 +66,9 @@ type coqargs_pre = {
 
   ml_includes : string list;
   vo_includes : Loadpath.vo_path list;
-  vo_requires : (string * string option * bool option) list;
-  (* None = No Import; Some false = Import; Some true = Export *)
 
   load_vernacular_list : (string * bool) list;
+  injections  : Stm.injection_command list;
 
   inputstate  : string option;
 }
@@ -124,7 +120,6 @@ let default_config = {
   debug        = false;
   time         = false;
   print_emacs  = false;
-  set_options  = [];
 
   (* Quiet / verbosity options should be here *)
 }
@@ -135,8 +130,8 @@ let default_pre = {
   load_rcfile  = true;
   ml_includes  = [];
   vo_includes  = [];
-  vo_requires  = [];
   load_vernacular_list = [];
+  injections   = [];
   inputstate   = None;
 }
 
@@ -167,13 +162,13 @@ let add_vo_include opts unix_path coq_path implicit =
         unix_path; coq_path; has_ml = false; implicit; recursive = true } :: opts.pre.vo_includes }}
 
 let add_vo_require opts d p export =
-  { opts with pre = { opts.pre with vo_requires = (d, p, export) :: opts.pre.vo_requires }}
+  { opts with pre = { opts.pre with injections = Stm.RequireInjection (d, p, export) :: opts.pre.injections }}
 
 let add_load_vernacular opts verb s =
-  { opts with pre = { opts.pre with load_vernacular_list = (CUnix.make_suffix s ".v",verb) :: opts.pre.load_vernacular_list }}
+    { opts with pre = { opts.pre with load_vernacular_list = (CUnix.make_suffix s ".v",verb) :: opts.pre.load_vernacular_list }}
 
 let add_set_option opts opt_name value =
-  { opts with config = { opts.config with set_options = (opt_name, value) :: opts.config.set_options }}
+  { opts with pre = { opts.pre with injections = Stm.OptionInjection (opt_name, value) :: opts.pre.injections }}
 
 (** Options for proof general *)
 let set_emacs opts =
@@ -486,10 +481,10 @@ let parse_args ~help ~init arglist : t * string list =
 
     | "-set" ->
       let opt, v = parse_option_set @@ next() in
-      add_set_option oval opt (OptionSet v)
+      add_set_option oval opt (Stm.OptionSet v)
 
     | "-unset" ->
-      add_set_option oval (to_opt_key @@ next ()) OptionUnset
+      add_set_option oval (to_opt_key @@ next ()) Stm.OptionUnset
 
     |"-native-output-dir" ->
       let native_output_dir = next () in
@@ -513,18 +508,18 @@ let parse_args ~help ~init arglist : t * string list =
     |"-config"|"--config" -> set_query oval PrintConfig
     |"-debug" -> Coqinit.set_debug (); oval
     |"-diffs" ->
-      add_set_option oval Proof_diffs.opt_name @@ OptionSet (Some (next ()))
+      add_set_option oval Proof_diffs.opt_name @@ Stm.OptionSet (Some (next ()))
     |"-stm-debug" -> Stm.stm_debug := true; oval
     |"-emacs" -> set_emacs oval
     |"-impredicative-set" ->
       set_logic (fun o -> { o with impredicative_set = Declarations.ImpredicativeSet }) oval
     |"-allow-sprop" ->
-      add_set_option oval Vernacentries.allow_sprop_opt_name (OptionSet None)
+      add_set_option oval Vernacentries.allow_sprop_opt_name (Stm.OptionSet None)
     |"-disallow-sprop" ->
-      add_set_option oval Vernacentries.allow_sprop_opt_name OptionUnset
+      add_set_option oval Vernacentries.allow_sprop_opt_name Stm.OptionUnset
     |"-sprop-cumulative" ->
       warn_deprecated_sprop_cumul();
-      add_set_option oval Vernacentries.cumul_sprop_opt_name (OptionSet None)
+      add_set_option oval Vernacentries.cumul_sprop_opt_name (Stm.OptionSet None)
     |"-indices-matter" -> set_logic (fun o -> { o with indices_matter = true }) oval
     |"-m"|"--memory" -> { oval with post = { oval.post with memory_stat = true }}
     |"-noinit"|"-nois" -> { oval with pre = { oval.pre with load_init = false }}
@@ -564,12 +559,9 @@ let parse_args ~help ~init args =
       pre = { opts.pre with
               ml_includes = List.rev opts.pre.ml_includes
             ; vo_includes = List.rev opts.pre.vo_includes
-            ; vo_requires = List.rev opts.pre.vo_requires
             ; load_vernacular_list = List.rev opts.pre.load_vernacular_list
+            ; injections = List.rev opts.pre.injections
             }
-    ; config = { opts.config with
-                 set_options = List.rev opts.config.set_options
-               } ;
     } in
   opts, extra
 
@@ -579,8 +571,8 @@ let parse_args ~help ~init args =
 (* prelude_data == From Coq Require Import Prelude. *)
 let prelude_data = "Prelude", Some "Coq", Some false
 
-let require_libs opts =
-  if opts.pre.load_init then prelude_data :: opts.pre.vo_requires else opts.pre.vo_requires
+let injection_commands opts =
+  if opts.pre.load_init then Stm.RequireInjection prelude_data :: opts.pre.injections else opts.pre.injections
 
 let build_load_path opts =
   let ml_path, vo_path =
diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli
index a51ed6766a..c8634b7847 100644
--- a/toplevel/coqargs.mli
+++ b/toplevel/coqargs.mli
@@ -14,8 +14,6 @@ val default_toplevel : Names.DirPath.t
 
 type native_compiler = NativeOff | NativeOn of { ondemand : bool }
 
-type option_command = OptionSet of string option | OptionUnset
-
 type coqargs_logic_config = {
   impredicative_set : Declarations.set_predicativity;
   indices_matter    : bool;
@@ -35,7 +33,6 @@ type coqargs_config = {
   debug       : bool;
   time        : bool;
   print_emacs : bool;
-  set_options : (Goptions.option_name * option_command) list;
 }
 
 type coqargs_pre = {
@@ -45,10 +42,10 @@ type coqargs_pre = {
 
   ml_includes : CUnix.physical_path list;
   vo_includes : Loadpath.vo_path list;
-  vo_requires : (string * string option * bool option) list;
-  (* None = No Import; Some false = Import; Some true = Export *)
 
   load_vernacular_list : (string * bool) list;
+  injections  : Stm.injection_command list;
+
   inputstate  : string option;
 }
 
@@ -79,5 +76,5 @@ val default : t
 val parse_args : help:Usage.specific_usage -> init:t -> string list -> t * string list
 val error_wrong_arg : string -> unit
 
-val require_libs : t -> (string * string option * bool option) list
+val injection_commands : t -> Stm.injection_command list
 val build_load_path : t -> CUnix.physical_path list * Loadpath.vo_path list
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 7aad856d0a..2d450d430a 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -243,13 +243,13 @@ let init_document opts =
   (* Next line allows loading .vos files when in interactive mode *)
   Flags.load_vos_libraries := true;
   let ml_load_path, vo_load_path = build_load_path opts in
-  let require_libs = require_libs opts in
+  let injections = injection_commands opts in
   let stm_options = opts.config.stm_flags in
   let open Vernac.State in
   let doc, sid =
     Stm.(new_doc
            { doc_type = Interactive opts.config.logic.toplevel_name;
-             ml_load_path; vo_load_path; require_libs; stm_options;
+             ml_load_path; vo_load_path; injections; stm_options;
            }) in
   { doc; sid; proof = None; time = opts.config.time }
 
@@ -273,7 +273,6 @@ type run_mode = Interactive | Batch
 let init_toploop opts =
   let state = init_document opts in
   let state = Ccompile.load_init_vernaculars opts ~state in
-  Ccompile.set_options opts.config.set_options;
   state
 
 let coqtop_init run_mode ~opts =