Skip to content

Commit

Permalink
Redesign Goptions API
Browse files Browse the repository at this point in the history
- 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)

- expose API for unsynchronized options (would allow to fix the code
  in MetaCoq/metacoq#1123 instead of removing it)
  • Loading branch information
SkySkimmer committed Jan 14, 2025
1 parent 1c962f3 commit a5148e7
Show file tree
Hide file tree
Showing 13 changed files with 336 additions and 208 deletions.
2 changes: 1 addition & 1 deletion ide/rocqide/idetop.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Loading

0 comments on commit a5148e7

Please sign in to comment.