Remove Goptions.opt_name field

The standard use is to repeat the option keywords in lowercase, which
is basically useless.

En passant add doc entry for Dump Arith.

1 files changed, 0 insertions, 2 deletions

diff --git a/ide/protocol/interface.ml b/ide/protocol/interface.ml
index 362833743e..be5e305ad3 100644
--- a/ide/protocol/interface.ml
+++ b/ide/protocol/interface.ml
@@ -71,8 +71,6 @@ type option_state = {
   (** Whether an option is synchronous *)
   opt_depr  : bool;
   (** Whether an option is deprecated *)
-  opt_name  : string;
-  (** A short string that is displayed when using [Test] *)
   opt_value : option_value;
   (** The current value of the option *)
 }