Redesign Goptions API

- use GADT to control the type of the value - remove "Set ... Append" command, instead appending is a behaviour of the given option (currently Warnings and Debug)
SkySkimmer · Jan 22, 2025 · ec9b66a · ec9b66a
1 parent c1d8bee
commit ec9b66a
Show file tree

Hide file tree

Showing 13 changed files with 298 additions and 208 deletions.
diff --git 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