From 4563779bf990cf22d88474a68acf4eb9cfd8d173 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 4 Feb 2020 17:07:34 +0100
Subject: 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.
---
 printing/printer.ml     | 5 -----
 printing/printmod.ml    | 1 -
 printing/proof_diffs.ml | 1 -
 3 files changed, 7 deletions(-)

(limited to 'printing')

diff --git a/printing/printer.ml b/printing/printer.ml
index 8af4d1d932..cc83a1dde0 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -38,7 +38,6 @@ let () =
   let open Goptions in
   declare_bool_option
     { optdepr  = false;
-      optname  = "printing of unfocused goal";
       optkey   = ["Printing";"Unfocused"];
       optread  = (fun () -> !enable_unfocused_goal_printing);
       optwrite = (fun b -> enable_unfocused_goal_printing:=b) }
@@ -49,7 +48,6 @@ let () =
   let open Goptions in
   declare_bool_option
     { optdepr  = false;
-      optname  = "printing of goal tags";
       optkey   = ["Printing";"Goal";"Tags"];
       optread  = (fun () -> !enable_goal_tags_printing);
       optwrite = (fun b -> enable_goal_tags_printing:=b) }
@@ -59,7 +57,6 @@ let () =
   let open Goptions in
   declare_bool_option
     { optdepr  = false;
-      optname  = "printing of goal names";
       optkey   = ["Printing";"Goal";"Names"];
       optread  = (fun () -> !enable_goal_names_printing);
       optwrite = (fun b -> enable_goal_names_printing:=b) }
@@ -416,7 +413,6 @@ let () =
   let open Goptions in
   declare_int_option
     { optdepr  = false;
-      optname  = "the hypotheses limit";
       optkey   = ["Hyps";"Limit"];
       optread  = (fun () -> !print_hyps_limit);
       optwrite = (fun x -> print_hyps_limit := x) }
@@ -625,7 +621,6 @@ let () =
   let open Goptions in
   declare_bool_option
     { optdepr  = false;
-      optname  = "Printing Dependent Evars Line";
       optkey   = ["Printing";"Dependent";"Evars";"Line"];
       optread  = (fun () -> !should_print_dependent_evars);
       optwrite = (fun v -> should_print_dependent_evars := v) }
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 85bb287c22..a5fd7f69ed 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -44,7 +44,6 @@ let short = ref false
 let () =
   declare_bool_option
     { optdepr  = false;
-      optname  = "short module printing";
       optkey   = ["Short";"Module";"Printing"];
       optread  = (fun () -> !short) ;
       optwrite = ((:=) short) }
diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
index dec87f8071..d93dd15f91 100644
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.ml
@@ -69,7 +69,6 @@ let write_diffs_option opt =
 let () =
   Goptions.(declare_string_option {
     optdepr = false;
-    optname = "show diffs in proofs";
     optkey = ["Diffs"];
     optread = read_diffs_option;
     optwrite = write_diffs_option
-- 
cgit v1.2.3