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, 1 deletions

diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index dce0a70f72..d711c9aea0 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -42,7 +42,6 @@ let should_auto_template =
   let auto = ref true in
   let () = declare_bool_option
       { optdepr  = false;
-        optname  = "Automatically make some inductive types template polymorphic";
         optkey   = ["Auto";"Template";"Polymorphism"];
         optread  = (fun () -> !auto);
         optwrite = (fun b -> auto := b); }