diff --git a/ide/rocqide/idetop.ml b/ide/rocqide/idetop.ml
index cc123e71267a..63143667e445 100644
--- a/ide/rocqide/idetop.ml
+++ b/ide/rocqide/idetop.ml
@@ -703,7 +703,7 @@ let islave_init ( { Coqtop.run_mode; color_mode }, stm_opts) injections ~opts =
   if run_mode = Coqtop.Batch then Flags.quiet := true;
   (* -xml-debug implies -debug. *)
   let injections = if !Flags.xml_debug
-    then Coqargs.OptionInjection (["Debug"], OptionAppend "all") :: injections
+    then Coqargs.OptionInjection (["Debug"], OptionSet (Some "all")) :: injections
     else injections
   in
   Coqtop.init_toploop opts stm_opts injections
diff --git a/library/goptions.ml b/library/goptions.ml
index d771f16830af..a66b362c1a75 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -14,6 +14,13 @@ open Util
 open Summary.Stage
 
 type option_name = string list
+
+type _ option_kind =
+  | BoolKind : bool option_kind
+  | IntKind : int option option_kind
+  | StringKind : string option_kind
+  | StringOptKind : string option option_kind
+
 type option_value =
   | BoolValue   of bool
   | IntValue    of int option
@@ -225,17 +232,8 @@ let iter_table env f key lv =
 (****************************************************************************)
 (* 2- Flags.                                                              *)
 
-type 'a option_sig = {
-  optstage : Summary.Stage.t;
-  optdepr  : Deprecation.t option;
-  optkey   : option_name;
-  optread  : unit -> 'a;
-  optwrite : 'a -> unit }
-
 type option_locality = OptDefault | OptLocal | OptExport | OptGlobal
 
-type option_mod = OptSet | OptAppend
-
 module OptionOrd =
 struct
   type t = option_name
@@ -244,6 +242,18 @@ end
 
 module OptionMap = Map.Make(OptionOrd)
 
+module RawOpt = struct
+  type 'a t = {
+    kind : 'a option_kind;
+    depr : Deprecation.t option;
+    stage : Summary.Stage.t;
+    read : unit -> 'a;
+    write : option_locality -> 'a -> unit;
+  }
+end
+
+type any_opt = AnyOpt : 'a RawOpt.t -> any_opt
+
 let value_tab = ref OptionMap.empty
 
 (* This raises Not_found if option of key [key] is unknown *)
@@ -260,84 +270,111 @@ with Not_found ->
   then CErrors.user_err Pp.(str "Sorry, this option name ("
     ++ str (nickname key) ++ str ") is already used.")
 
+let declare_raw name v = value_tab := OptionMap.add name (AnyOpt v) !value_tab
+
+let declare_unsynchronized_option name v =
+  check_key name;
+  declare_raw name v
+
+(* not quite the same as RawOpt.t: write takes a option_locality, optkey field present *)
+type 'a option_sig = {
+  optkind : 'a option_kind;
+  optstage : Summary.Stage.t;
+  optdepr  : Deprecation.t option;
+  optkey   : option_name;
+  optread  : unit -> 'a;
+  optwrite : 'a -> unit }
+
 open Libobject
 
 let warn_deprecated_option =
   Deprecation.create_warning ~object_name:"Option" ~warning_name_if_no_since:"deprecated-option"
     (fun key -> Pp.str (nickname key))
 
-let declare_option cast uncast append ?(preprocess = fun x -> x)
-  { optstage=stage; optdepr=depr; optkey=key; optread=read; optwrite=write } =
+let option_object name stage act =
+  let cache_option (l,v) = act v in
+  let load_option i (l, _ as o) = match l with
+    | OptGlobal -> cache_option o
+    | OptExport -> ()
+    | OptLocal | OptDefault ->
+      (* Ruled out by classify_function *)
+      assert false
+  in
+  let open_option i  (l, _ as o) = match l with
+    | OptExport -> if Int.equal i 1 then cache_option o
+    | OptGlobal -> ()
+    | OptLocal | OptDefault ->
+      (* Ruled out by classify_function *)
+      assert false
+  in
+  let discharge_option (l,_ as o) =
+    match l with OptLocal -> None | (OptExport | OptGlobal | OptDefault) -> Some o
+  in
+  let classify_option (l,_) =
+    match l with (OptExport | OptGlobal) -> Substitute | (OptLocal | OptDefault) -> Dispose
+  in
+  { (Libobject.default_object name) with
+    object_stage = stage;
+    cache_function = cache_option;
+    load_function = load_option;
+    open_function = simple_open ~cat:opts_cat open_option;
+    subst_function = (fun (_,o) -> o);
+    discharge_function = discharge_option;
+    classify_function = classify_option;
+  }
+
+let declare_option ?(preprocess = fun x -> x)
+  { optkind=kind; optstage=stage; optdepr=depr; optkey=key; optread=read; optwrite=write } =
   check_key key;
   let default = read() in
+  let () = Summary.declare_summary (nickname key)
+      { stage;
+        Summary.freeze_function = read;
+        Summary.unfreeze_function = write;
+        Summary.init_function = (fun () -> write default) }
+  in
   let change =
-      let () = Summary.declare_summary (nickname key)
-        { stage;
-          Summary.freeze_function = read;
-          Summary.unfreeze_function = write;
-          Summary.init_function = (fun () -> write default) } in
-      let cache_options (l,m,v) =
-        match m with
-        | OptSet -> write v
-        | OptAppend -> write (append (read ()) v) in
-      let load_options i (l, _, _ as o) = match l with
-      | OptGlobal -> cache_options o
-      | OptExport -> ()
-      | OptLocal | OptDefault ->
-        (* Ruled out by classify_function *)
-        assert false
+      let options : option_locality * _ -> obj =
+        declare_object (option_object (nickname key) stage write)
       in
-      let open_options i  (l, _, _ as o) = match l with
-      | OptExport -> if Int.equal i 1 then cache_options o
-      | OptGlobal -> ()
-      | OptLocal | OptDefault ->
-        (* Ruled out by classify_function *)
-        assert false
+      (fun l v -> let v = preprocess v in Lib.add_leaf (options (l, v)))
+  in
+  let warn () = depr |> Option.iter (fun depr -> warn_deprecated_option (key,depr)) in
+  let cwrite l v = warn (); change l v in
+  declare_raw key {
+    kind;
+    stage;
+    depr;
+    read;
+    write = cwrite;
+  }
+
+let declare_append_only_option ?(preprocess= fun x -> x) ~sep
+    { optkind=kind; optstage=stage; optdepr=depr; optkey=key; optread=read; optwrite=write } =
+  check_key key;
+  let default = read() in
+  let () = Summary.declare_summary (nickname key)
+      { stage;
+        Summary.freeze_function = read;
+        Summary.unfreeze_function = write;
+        Summary.init_function = (fun () -> write default) }
+  in
+  let append x = write (read()^sep^x) in
+  let change =
+      let options : option_locality * _ -> obj =
+        declare_object (option_object (nickname key) stage append)
       in
-      let subst_options (subst,obj) = obj in
-      let discharge_options (l,_,_ as o) =
-        match l with OptLocal -> None | (OptExport | OptGlobal | OptDefault) -> Some o in
-      let classify_options (l,_,_) =
-        match l with (OptExport | OptGlobal) -> Substitute | (OptLocal | OptDefault) -> Dispose in
-      let options : option_locality * option_mod * _ -> obj =
-        declare_object
-          { (default_object (nickname key)) with
-            object_stage = stage;
-            load_function = load_options;
-            open_function = simple_open ~cat:opts_cat open_options;
-            cache_function = cache_options;
-            subst_function = subst_options;
-            discharge_function = discharge_options;
-            classify_function = classify_options } in
-      (fun l m v -> let v = preprocess v in Lib.add_leaf (options (l, m, v)))
+      (fun l v -> let v = preprocess v in Lib.add_leaf (options (l, v)))
   in
   let warn () = depr |> Option.iter (fun depr -> warn_deprecated_option (key,depr)) in
-  let cread () = cast (read ()) in
-  let cwrite l v = warn (); change l OptSet (uncast v) in
-  let cappend l v = warn (); change l OptAppend (uncast v) in
-  value_tab := OptionMap.add key (depr, stage, (cread,cwrite,cappend)) !value_tab
-
-let declare_int_option =
-  declare_option
-    (fun v -> IntValue v)
-    (function IntValue v -> v | _ -> CErrors.anomaly (Pp.str "async_option."))
-    (fun _ _ -> CErrors.anomaly (Pp.str "async_option."))
-let declare_bool_option =
-  declare_option
-    (fun v -> BoolValue v)
-    (function BoolValue v -> v | _ -> CErrors.anomaly (Pp.str "async_option."))
-    (fun _ _ -> CErrors.anomaly (Pp.str "async_option."))
-let declare_string_option =
-  declare_option
-    (fun v -> StringValue v)
-    (function StringValue v -> v | _ -> CErrors.anomaly (Pp.str "async_option."))
-    (fun x y -> x^","^y)
-
-let declare_stringopt_option =
-  declare_option
-    (fun v -> StringOptValue v)
-    (function StringOptValue v -> v | _ -> CErrors.anomaly (Pp.str "async_option."))
-    (fun _ _ -> CErrors.anomaly (Pp.str "async_option."))
+  let cwrite l v = warn (); change l v in
+  declare_raw key {
+    kind;
+    stage;
+    depr;
+    read;
+    write = cwrite;
+  }
 
 type 'a getter = { get : unit -> 'a }
 
@@ -347,7 +384,8 @@ let declare_int_option_and_ref ?(stage=Interp) ?depr ~key ~(value:int) () =
   let r_opt = ref value in
   let optwrite v = r_opt := Option.default value v in
   let optread () = Some !r_opt in
-  let () = declare_int_option {
+  let () = declare_option {
+      optkind = IntKind;
       optstage = stage;
       optdepr = depr;
       optkey = key;
@@ -360,7 +398,8 @@ let declare_intopt_option_and_ref ?(stage=Interp) ?depr ~key ~value () =
   let r_opt = ref value in
   let optwrite v = r_opt := v in
   let optread () = !r_opt in
-  let () = declare_int_option {
+  let () = declare_option {
+      optkind = IntKind;
       optstage = stage;
       optdepr = depr;
       optkey = key;
@@ -378,7 +417,8 @@ let declare_nat_option_and_ref ?(stage=Interp) ?depr ~key ~(value:int) () =
     r_opt := v
   in
   let optread () = Some !r_opt in
-  let () = declare_int_option {
+  let () = declare_option {
+      optkind = IntKind;
       optstage = stage;
       optdepr = depr;
       optkey = key;
@@ -390,7 +430,8 @@ let declare_bool_option_and_ref ?(stage=Interp) ?depr ~key ~(value:bool) () =
   let r_opt = ref value in
   let optwrite v = r_opt := v in
   let optread () = !r_opt in
-  let () = declare_bool_option {
+  let () = declare_option {
+      optkind = BoolKind;
       optstage = stage;
       optdepr = depr;
       optkey = key;
@@ -402,7 +443,8 @@ let declare_string_option_and_ref ?(stage=Interp) ?depr ~key ~(value:string) ()
   let r_opt = ref value in
   let optwrite v = r_opt := Option.default value v in
   let optread () = Some !r_opt in
-  let () = declare_stringopt_option {
+  let () = declare_option {
+      optkind = StringOptKind;
       optstage = stage;
       optdepr = depr;
       optkey = key;
@@ -414,7 +456,8 @@ let declare_stringopt_option_and_ref ?(stage=Interp) ?depr ~key ~value () =
   let r_opt = ref value in
   let optwrite v = r_opt := v in
   let optread () = !r_opt in
-  let () = declare_stringopt_option {
+  let () = declare_option {
+      optkind = StringOptKind;
       optstage = stage;
       optdepr = depr;
       optkey = key;
@@ -426,7 +469,8 @@ let declare_interpreted_string_option_and_ref from_string to_string ?(stage=Inte
   let r_opt = ref value in
   let optwrite v = r_opt := Option.default value @@ Option.map from_string v in
   let optread () = Some (to_string !r_opt) in
-  let () = declare_stringopt_option {
+  let () = declare_option {
+      optkind = StringOptKind;
       optstage = stage;
       optdepr = depr;
       optkey = key;
@@ -444,23 +488,19 @@ let warn_unknown_option =
     Pp.(fun key -> strbrk "There is no flag or option with this name: \"" ++
                   str (nickname key) ++ str "\".")
 
+let to_option_value (type a) (k:a option_kind) (v:a) : option_value =
+  match k with
+  | BoolKind -> BoolValue v
+  | IntKind -> IntValue v
+  | StringKind -> StringValue v
+  | StringOptKind -> StringOptValue v
+
 let get_option_value key =
   try
-    let (_,_,(read,write,append)) = get_option key in
-    Some read
+    let AnyOpt opt = get_option key in
+    Some (fun () -> to_option_value opt.kind (opt.read ()))
   with Not_found -> None
 
-(** Sets the option only if [stage] matches the option declaration or if [stage]
-  is omitted. If the option is not found, a warning is emitted only if the stage
-  is [Interp] or omitted. *)
-let set_option_value ?(locality = OptDefault) ?stage check_and_cast key v =
-  let opt = try Some (get_option key) with Not_found -> None in
-  match opt with
-  | None -> begin match stage with None | Some Summary.Stage.Interp -> warn_unknown_option key | _ -> () end
-  | Some (depr, option_stage, (read,write,append)) ->
-    if Option.cata (fun s -> s = option_stage) true stage then
-      write locality (check_and_cast v (read ()))
-
 let bad_type_error ~expected ~got =
   CErrors.user_err Pp.(strbrk "Bad type of value for this option:" ++ spc()
     ++ str "expected " ++ str expected ++ str ", got " ++ str got ++ str ".")
@@ -468,29 +508,45 @@ let bad_type_error ~expected ~got =
 let error_flag () =
   CErrors.user_err Pp.(str "This is a flag. It does not take a value.")
 
-let check_int_value v = function
-  | BoolValue _ -> error_flag ()
-  | IntValue _ -> IntValue v
-  | StringValue _ | StringOptValue _ ->
-     bad_type_error ~expected:"string" ~got:"int"
+type 'a check_and_cast = { check_and_cast : 'b. 'a -> 'b option_kind -> 'b }
 
-let check_bool_value v = function
-  | BoolValue _ -> BoolValue v
+(** Sets the option only if [stage] matches the option declaration or if [stage]
+  is omitted. If the option is not found, a warning is emitted only if the stage
+  is [Interp] or omitted. *)
+let set_option_value ?(locality = OptDefault) ?stage { check_and_cast } key v =
+  match get_option key with
+  | exception Not_found -> begin match stage with None | Some Summary.Stage.Interp -> warn_unknown_option key | _ -> () end
+  | AnyOpt opt ->
+    if Option.cata (fun s -> s = opt.stage) true stage then
+      opt.write locality (check_and_cast v opt.kind)
+
+let check_int_value (type a) (v:int option) (k:a option_kind) : a =
+  match k with
+  | BoolKind -> error_flag ()
+  | IntKind -> v
+  | StringKind | StringOptKind ->
+    bad_type_error ~expected:"string" ~got:"int"
+
+let check_bool_value (type a) (v:bool) (k:a option_kind) : a =
+  match k with
+  | BoolKind -> v
   | _ ->
-      CErrors.user_err
-        Pp.(str "This is an option. A value must be provided.")
-
-let check_string_value v = function
-  | BoolValue _ -> error_flag ()
-  | IntValue _ -> bad_type_error ~expected:"int" ~got:"string"
-  | StringValue _ -> StringValue v
-  | StringOptValue _ -> StringOptValue (Some v)
-
-let check_unset_value v = function
-  | BoolValue _ -> BoolValue false
-  | IntValue _ -> IntValue None
-  | StringOptValue _ -> StringOptValue None
-  | StringValue _ ->
+    CErrors.user_err
+      Pp.(str "This is an option. A value must be provided.")
+
+let check_string_value (type a) (v:string) (k:a option_kind) : a =
+  match k with
+  | BoolKind -> error_flag ()
+  | IntKind -> bad_type_error ~expected:"int" ~got:"string"
+  | StringKind -> v
+  | StringOptKind -> (Some v)
+
+let check_unset_value (type a) () (k:a option_kind) : a =
+  match k with
+  | BoolKind -> false
+  | IntKind -> None
+  | StringOptKind -> None
+  | StringKind ->
       CErrors.user_err
         Pp.(str "This option does not support the \"Unset\" command.")
 
@@ -499,21 +555,13 @@ let check_unset_value v = function
    exist anymore *)
 
 let set_int_option_value_gen ?locality ?stage =
-  set_option_value ?locality ?stage check_int_value
+  set_option_value ?locality ?stage { check_and_cast = check_int_value }
 let set_bool_option_value_gen ?locality ?stage key v =
-  set_option_value ?locality ?stage check_bool_value key v
+  set_option_value ?locality ?stage { check_and_cast = check_bool_value } key v
 let set_string_option_value_gen ?locality ?stage =
-  set_option_value ?locality ?stage check_string_value
+  set_option_value ?locality ?stage { check_and_cast = check_string_value }
 let unset_option_value_gen ?locality ?stage key =
-  set_option_value ?locality ?stage check_unset_value key ()
-
-let set_string_option_append_value_gen ?(locality = OptDefault) ?stage key v =
-  let opt = try Some (get_option key) with Not_found -> None in
-  match opt with
-  | None -> warn_unknown_option key
-  | Some (depr, option_stage, (read,write,append)) ->
-    if Option.cata (fun s -> s = option_stage) true stage then
-      append locality (check_string_value v (read ()))
+  set_option_value ?locality ?stage { check_and_cast = check_unset_value } key ()
 
 let set_int_option_value ?stage opt v = set_int_option_value_gen ?stage opt v
 let set_bool_option_value ?stage opt v = set_bool_option_value_gen ?stage opt v
@@ -531,22 +579,22 @@ let msg_option_value = Pp.(function
   | StringOptValue (Some s) -> quote (str s))
 
 let print_option_value key =
-  let (depr, _stage, (read,_,_)) = get_option key in
-  let s = read () in
-  match s with
+  let AnyOpt opt = get_option key in
+  let s = opt.read () in
+  match to_option_value opt.kind s with
     | BoolValue b ->
         Feedback.msg_notice Pp.(prlist_with_sep spc str key ++ str " is "
           ++ str (if b then "on" else "off"))
-    | _ ->
+    | s ->
         Feedback.msg_notice Pp.(str "Current value of "
           ++ prlist_with_sep spc str key ++ str " is " ++ msg_option_value s)
 
 let get_tables () =
   let tables = !value_tab in
-  let fold key (depr, _stage, (read,_,_)) accu =
+  let fold key (AnyOpt opt) accu =
     let state = {
-      opt_depr = depr;
-      opt_value = read ();
+      opt_depr = opt.depr;
+      opt_value = to_option_value opt.kind (opt.read ());
     } in
     OptionMap.add key state accu
   in
@@ -568,8 +616,8 @@ let print_tables () =
   in
   str "Options:" ++ fnl () ++
     OptionMap.fold
-      (fun key (depr, _stage, (read,_,_)) p ->
-        p ++ print_option key (read ()) depr)
+      (fun key (AnyOpt opt) p ->
+        p ++ print_option key (to_option_value opt.kind (opt.read ())) opt.depr)
       !value_tab (mt ()) ++
   str "Tables:" ++ fnl () ++
     List.fold_right
@@ -579,3 +627,38 @@ let print_tables () =
       (fun (nickkey,_) p -> p ++ str "  " ++ str nickkey ++ fnl ())
       !ref_table (mt ()) ++
     fnl ()
+
+(* Compat *)
+
+module OldSig = struct
+  type 'a t = {
+    optstage   : Summary.Stage.t;
+    optdepr    : Deprecation.t option;
+    (** whether the option is DEPRECATED *)
+    optkey     : option_name;
+    (** the low-level name of this option *)
+    optread    : unit -> 'a;
+    optwrite   : 'a -> unit
+  }
+end
+
+let newsig kind (oldsig:_ OldSig.t) = {
+  optkind = kind;
+  optstage = oldsig.optstage;
+  optdepr = oldsig.optdepr;
+  optkey = oldsig.optkey;
+  optread = oldsig.optread;
+  optwrite = oldsig.optwrite;
+}
+
+let declare_int_option ?preprocess oldsig =
+  declare_option ?preprocess (newsig IntKind oldsig)
+
+let declare_bool_option ?preprocess oldsig =
+  declare_option ?preprocess (newsig BoolKind oldsig)
+
+let declare_string_option ?preprocess oldsig =
+  declare_option ?preprocess (newsig StringKind oldsig)
+
+let declare_stringopt_option ?preprocess oldsig =
+  declare_option ?preprocess (newsig StringOptKind oldsig)
diff --git a/library/goptions.mli b/library/goptions.mli
index dd97ffd6d5f1..9fc20a885fc8 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -47,6 +47,12 @@
 
 type option_name = string list
 
+type _ option_kind =
+  | BoolKind : bool option_kind
+  | IntKind : int option option_kind
+  | StringKind : string option_kind
+  | StringOptKind : string option option_kind
+
 type option_locality = OptDefault | OptLocal | OptExport | OptGlobal
 
 (** {6 Tables. } *)
@@ -114,11 +120,12 @@ end
    "Print Toto Titi."
 
    The declare_*_option functions are low-level, to be used when
-   implementing complex option workflows, e.g. when setting one option
-   changes the value of another.  For most use cases, you should use
+   implementing complex option workflows, e.g. when the option data is in the global env.
+   For most use cases, you should use
    the helper functions declare_*_option_and_ref. *)
 
 type 'a option_sig = {
+  optkind : 'a option_kind;
   optstage   : Summary.Stage.t;
   optdepr    : Deprecation.t option;
   (** whether the option is DEPRECATED *)
@@ -131,18 +138,45 @@ type 'a option_sig = {
 (** The [preprocess] function is triggered before setting the option. It can be
     used to emit a warning on certain values, and clean-up the final value.
 
-    [declare_stringopt_option] should be preferred to [declare_string_option]
-    because it supports "Unset".
-    Only "Warnings" option is declared using the latter.*)
+    [StringOptKind] should be preferred to [StringKind] because it supports "Unset". *)
+val declare_option   : ?preprocess:('a -> 'a) -> 'a option_sig -> unit
+
+val declare_append_only_option : ?preprocess:(string -> string) -> sep:string ->
+  string option_sig -> unit
+
+(** Unsynchronized options *)
+module RawOpt : sig
+  type 'a t = {
+    kind : 'a option_kind;
+    depr : Deprecation.t option;
+    stage : Summary.Stage.t;
+    read : unit -> 'a;
+    write : option_locality -> 'a -> unit;
+  }
+end
 
-val declare_int_option   : ?preprocess:(int option -> int option) ->
-                           int option option_sig -> unit
-val declare_bool_option  : ?preprocess:(bool -> bool) ->
-                           bool option_sig   -> unit
-val declare_string_option: ?preprocess:(string -> string) ->
-                           string option_sig -> unit
-val declare_stringopt_option: ?preprocess:(string option -> string option) ->
-                              string option option_sig -> unit
+(** Declare an unsynchronized option.
+    This means that [write] is called directly by "Set Foo" (after type casting).
+
+    This is in particular useful to define options which wrap another option,
+    eg suppose "Foo Debug Verbosity" is from [declare_intopt_option_and_ref]
+    and we want to declare a flag "Foo Debug" which when unset will unset "Foo Debug Verbosity",
+    and when set will set "Foo Debug Verbosity" to 1.
+    If we used [declare_option], backtracking would reset "Foo Debug Verbosity" and "Foo Debug"
+    in an undefined order, such that if "Foo Debug Verbosity" was 2
+    if "Foo Debug" is reset later it gets overwritted to 1.
+    ie "Set Foo Debug Verbosity 2. Something unrelated. Undo 1." may result in
+    "Foo Debug Verbosity = 1".
+
+    Therefore instead we should declare "Foo Debug" as an unsynchronized option, which calls
+    [set_int_option_value_gen] on "Foo Debug Verbosity"
+    (NB: the stage in [RawOpt.t] controls in which phase [write] is called).
+*)
+val declare_unsynchronized_option : option_name -> 'a RawOpt.t -> unit
+
+(** Helper to build synchronized options on top of [declare_unsynchronized_option]. *)
+val option_object : string -> Summary.Stage.t -> ('a -> unit) ->
+  (option_locality * 'b, option_locality * 'a, option_locality * 'b) Libobject.object_declaration
 
 (** Helpers to declare a reference controlled by an option. *)
 
@@ -182,7 +216,6 @@ val get_ref_table :
 val set_int_option_value_gen    : ?locality:option_locality -> ?stage:Summary.Stage.t -> option_name -> int option -> unit
 val set_bool_option_value_gen   : ?locality:option_locality -> ?stage:Summary.Stage.t -> option_name -> bool   -> unit
 val set_string_option_value_gen : ?locality:option_locality -> ?stage:Summary.Stage.t -> option_name -> string -> unit
-val set_string_option_append_value_gen : ?locality:option_locality -> ?stage:Summary.Stage.t -> option_name -> string -> unit
 val unset_option_value_gen : ?locality:option_locality -> ?stage:Summary.Stage.t -> option_name -> unit
 
 val set_int_option_value    : ?stage:Summary.Stage.t -> option_name -> int option -> unit
@@ -204,13 +237,14 @@ type table_value =
 (** [get_option_value key] returns [None] if option with name [key] was not found. *)
 val get_option_value : option_name -> (unit -> option_value) option
 
+type 'a check_and_cast = { check_and_cast : 'b. 'a -> 'b option_kind -> 'b }
+
 val set_option_value : ?locality:option_locality -> ?stage:Summary.Stage.t ->
-  ('a -> option_value -> option_value) -> option_name -> 'a -> unit
+  'a check_and_cast -> option_name -> 'a -> unit
 (** [set_option_value ?locality f name v] sets [name] to the result of
-    applying [f] to [v] and [name]'s current value. Use for behaviour
+    applying [f] to [v] and [name]'s option kind. Use for behaviour
     depending on the type of the option, eg erroring when ['a] doesn't
-    match it. Changing the type will result in errors later so don't do
-    that. *)
+    match it. *)
 
 (** Summary of an option status *)
 type option_state = {
@@ -225,3 +259,26 @@ type iter_table_aux = { aux : 'a. 'a table_of_A -> Environ.env -> 'a -> unit }
 val iter_table : Environ.env -> iter_table_aux -> option_name -> table_value list -> unit
 
 val error_undeclared_key : option_name -> 'a
+
+(** Compat *)
+
+module OldSig : sig
+  type 'a t = {
+    optstage   : Summary.Stage.t;
+    optdepr    : Deprecation.t option;
+    (** whether the option is DEPRECATED *)
+    optkey     : option_name;
+    (** the low-level name of this option *)
+    optread    : unit -> 'a;
+    optwrite   : 'a -> unit
+  }
+end
+
+val declare_int_option   : ?preprocess:(int option -> int option) ->
+                           int option OldSig.t -> unit
+val declare_bool_option  : ?preprocess:(bool -> bool) ->
+                           bool OldSig.t   -> unit
+val declare_string_option: ?preprocess:(string -> string) ->
+                           string OldSig.t -> unit
+val declare_stringopt_option: ?preprocess:(string option -> string option) ->
+                              string option OldSig.t -> unit
diff --git a/plugins/ltac2/tac2bt.ml b/plugins/ltac2/tac2bt.ml
index 2d1766bee7df..8b7e6ed71692 100644
--- a/plugins/ltac2/tac2bt.ml
+++ b/plugins/ltac2/tac2bt.ml
@@ -18,21 +18,21 @@ let backtrace : backtrace Exninfo.t = Exninfo.make "ltac2_trace"
 let print_ltac2_backtrace = ref false
 
 let () = Goptions.declare_bool_option {
-  Goptions.optstage = Summary.Stage.Interp;
-  Goptions.optdepr = None;
-  Goptions.optkey = ["Ltac2"; "Backtrace"];
-  Goptions.optread = (fun () -> !print_ltac2_backtrace);
-  Goptions.optwrite = (fun b -> print_ltac2_backtrace := b);
+  optstage = Summary.Stage.Interp;
+  optdepr = None;
+  optkey = ["Ltac2"; "Backtrace"];
+  optread = (fun () -> !print_ltac2_backtrace);
+  optwrite = (fun b -> print_ltac2_backtrace := b);
 }
 
 let ltac2_in_ltac1_profiling = ref false
 
 let () = Goptions.declare_bool_option {
-  Goptions.optstage = Summary.Stage.Interp;
-  Goptions.optdepr = None;
-  Goptions.optkey = ["Ltac2"; "In"; "Ltac1"; "Profiling"];
-  Goptions.optread = (fun () -> !ltac2_in_ltac1_profiling);
-  Goptions.optwrite = (fun b -> ltac2_in_ltac1_profiling := b);
+  optstage = Summary.Stage.Interp;
+  optdepr = None;
+  optkey = ["Ltac2"; "In"; "Ltac1"; "Profiling"];
+  optread = (fun () -> !ltac2_in_ltac1_profiling);
+  optwrite = (fun b -> ltac2_in_ltac1_profiling := b);
 }
 
 let get_backtrace =
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 79092e176d4b..f1d6759c2a48 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -49,11 +49,11 @@ let debug b =
   if b then pp_ref := ssr_pp else pp_ref := fun _ -> ()
 let _ =
   Goptions.declare_bool_option
-    { Goptions.optstage = Summary.Stage.Interp;
-      Goptions.optkey   = ["Debug";"SsrMatching"];
-      Goptions.optdepr  = None;
-      Goptions.optread  = (fun _ -> !pp_ref == ssr_pp);
-      Goptions.optwrite = debug }
+    { optstage = Summary.Stage.Interp;
+      optkey   = ["Debug";"SsrMatching"];
+      optdepr  = None;
+      optread  = (fun _ -> !pp_ref == ssr_pp);
+      optwrite = debug }
 let pp s = !pp_ref s
 
 (** Utils *)(* {{{ *****************************************************************)
diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml
index f4ba8246cc28..39295f9c5e08 100644
--- a/sysinit/coqargs.ml
+++ b/sysinit/coqargs.ml
@@ -33,7 +33,6 @@ type top = TopLogical of string | TopPhysical of string
 type option_command =
   | OptionSet of string option
   | OptionUnset
-  | OptionAppend of string
 
 type export_flag = Export | Import
 
@@ -186,7 +185,7 @@ let add_set_option opts opt_name value =
   { opts with pre = { opts.pre with injections = OptionInjection (opt_name, value) :: opts.pre.injections }}
 
 let add_set_debug opts flags =
-  add_set_option opts ["Debug"] (OptionAppend flags)
+  add_set_option opts ["Debug"] (OptionSet (Some flags))
 
 (** Options for proof general *)
 let set_emacs opts =
@@ -353,7 +352,7 @@ let parse_args ~init arglist : t * string list =
     |"-w" | "-W" ->
       let w = next () in
       if w = "none" then add_set_option oval ["Warnings"] (OptionSet(Some w))
-      else add_set_option oval ["Warnings"] (OptionAppend w)
+      else add_set_option oval ["Warnings"] (OptionSet (Some w))
 
     |"-bytecode-compiler" ->
       { oval with config = { oval.config with enable_VM = get_bool ~opt (next ()) }}
diff --git a/sysinit/coqargs.mli b/sysinit/coqargs.mli
index 0a550b76d584..68828b149a30 100644
--- a/sysinit/coqargs.mli
+++ b/sysinit/coqargs.mli
@@ -16,7 +16,6 @@ type top = TopLogical of string | TopPhysical of string
 type option_command =
   | OptionSet of string option
   | OptionUnset
-  | OptionAppend of string
 
 type export_flag = Export | Import
 
diff --git a/sysinit/coqinit.ml b/sysinit/coqinit.ml
index cdbb10ee29d3..c300a219f7f8 100644
--- a/sysinit/coqinit.ml
+++ b/sysinit/coqinit.ml
@@ -262,14 +262,16 @@ let warn_deprecated_native_compiler =
           Pp.strbrk "The native-compiler option is deprecated. To compile native \
           files ahead of time, use the coqnative binary instead.")
 
-let interp_set_option opt v old =
-  let open Goptions in
+let interp_set_option (type a) opt v (k:a Goptions.option_kind) : a =
   let opt = String.concat " " opt in
-  match old with
-  | BoolValue _ -> BoolValue (Coqargs.get_bool ~opt v)
-  | IntValue _ -> IntValue (Coqargs.get_int_opt ~opt v)
-  | StringValue _ -> StringValue v
-  | StringOptValue _ -> StringOptValue (Some v)
+  match k with
+  | BoolKind -> (Coqargs.get_bool ~opt v)
+  | IntKind -> (Coqargs.get_int_opt ~opt v)
+  | StringKind -> v
+  | StringOptKind -> Some v
+
+let interp_set_option opt =
+  { Goptions.check_and_cast = (fun v k -> interp_set_option opt v k ) }
 
 let set_option (opt,v) =
   let open Goptions in
@@ -277,7 +279,6 @@ let set_option (opt,v) =
   | OptionUnset -> unset_option_value_gen ~locality:OptLocal opt
   | OptionSet None -> set_bool_option_value_gen ~locality:OptLocal opt true
   | OptionSet (Some v) -> set_option_value ~locality:OptLocal (interp_set_option opt) opt v
-  | OptionAppend v -> set_string_option_append_value_gen ~locality:OptLocal opt v
 
 let handle_injection ~intern = let open Coqargs in function
   | RequireInjection {lib;prefix;export;allow_failure} ->
diff --git a/test-suite/bugs/bug_9453.v b/test-suite/bugs/bug_9453.v
index 18745533b201..93eb58d2c821 100644
--- a/test-suite/bugs/bug_9453.v
+++ b/test-suite/bugs/bug_9453.v
@@ -1,5 +1,5 @@
 (* check compatibility with 8.8 and earlier for lack of warnings on the nat 5000 *)
-Set Warnings Append "+large-nat,+abstract-large-number".
+Set Warnings "+large-nat,+abstract-large-number".
 Fail Check 5001.
 Check 5000.
 (* Error:
diff --git a/test-suite/output/NumberNotations.v b/test-suite/output/NumberNotations.v
index de84644790c6..6990d5c8042e 100644
--- a/test-suite/output/NumberNotations.v
+++ b/test-suite/output/NumberNotations.v
@@ -201,7 +201,7 @@ Module Test10.
   Delimit Scope unit_scope with unit.
   Delimit Scope unit2_scope with unit2.
   Number Notation unit of_uint to_uint (abstract after 0) : unit_scope.
-  Local Set Warnings Append "+abstract-large-number-no-op".
+  Local Set Warnings "+abstract-large-number-no-op".
   (* Check that there is actually a warning here *)
   Fail Number Notation unit of_uint to_uint (abstract after 0) : unit2_scope.
   (* Check that there is no warning here *)
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index a9f959d1baf2..d21147ad0310 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1966,16 +1966,18 @@ let () =
     CWarnings.check_unknown_warnings flags;
     CWarnings.normalize_flags_string flags
   in
-  declare_string_option ~preprocess
-    { optstage = Summary.Stage.Synterp;
+  declare_append_only_option ~preprocess ~sep:","
+    { optkind = StringKind;
+      optstage = Summary.Stage.Synterp;
       optdepr  = None;
       optkey   = ["Warnings"];
       optread  = CWarnings.get_flags;
       optwrite = CWarnings.set_flags }
 
 let () =
-  declare_string_option
-    { optstage = Summary.Stage.Synterp;
+  declare_append_only_option ~sep:","
+    { optkind = StringKind;
+      optstage = Summary.Stage.Synterp;
       optdepr  = None;
       optkey   = ["Debug"];
       optread  = CDebug.get_flags;
diff --git a/vernac/vernacoptions.ml b/vernac/vernacoptions.ml
index 2618a12460f0..b8454c06c81e 100644
--- a/vernac/vernacoptions.ml
+++ b/vernac/vernacoptions.ml
@@ -12,29 +12,19 @@ open Util
 open Goptions
 open Vernacexpr
 
-let vernac_set_option0 ~locality ~stage key opt =
+let vernac_set_option ~locality ~stage key opt =
   match opt with
   | OptionUnset -> unset_option_value_gen ~locality ~stage key
   | OptionSetString s -> set_string_option_value_gen ~locality ~stage key s
   | OptionSetInt n -> set_int_option_value_gen ~locality ~stage key (Some n)
   | OptionSetTrue -> set_bool_option_value_gen ~locality ~stage key true
 
-let vernac_set_append_option ~locality ~stage key s =
-  set_string_option_append_value_gen ~locality ~stage key s
-
-let vernac_set_option ~locality ~stage table v = match v with
-| OptionSetString s ->
-  (* We make a special case for warnings and debug flags because appending is
-  their natural semantics *)
-  if CString.List.equal table ["Warnings"] || CString.List.equal table ["Debug"] then
-    vernac_set_append_option ~locality ~stage table s
-  else
-    let (last, prefix) = List.sep_last table in
-    if String.equal last "Append" && not (List.is_empty prefix) then
-      vernac_set_append_option ~locality ~stage prefix s
-    else
-      vernac_set_option0 ~locality ~stage table v
-| _ -> vernac_set_option0 ~locality ~stage table v
+let vernac_set_option ~locality ~stage table v =
+  let () =
+    if String.equal "Append" (List.last table) then
+      CErrors.user_err Pp.(str "Set ... Append is not supported.");
+  in
+  vernac_set_option ~locality ~stage table v
 
 let iter_table f k v = Goptions.iter_table (Global.env()) f k v
 
diff --git a/vernac/vernacoptions.mli b/vernac/vernacoptions.mli
index e33932e02142..42de2c8292e4 100644
--- a/vernac/vernacoptions.mli
+++ b/vernac/vernacoptions.mli
@@ -10,9 +10,6 @@
 
 open Goptions
 
-val vernac_set_append_option :
-  locality:option_locality -> stage:Summary.Stage.t ->option_name -> string -> unit
-
 val vernac_set_option :
   locality:option_locality ->
   stage:Summary.Stage.t ->