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.
---
 vernac/proof_using.ml | 2 --
 1 file changed, 2 deletions(-)

(limited to 'vernac/proof_using.ml')

diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml
index cfb3248c7b..b329463cb0 100644
--- a/vernac/proof_using.ml
+++ b/vernac/proof_using.ml
@@ -140,7 +140,6 @@ let suggest_proof_using = ref false
 let () =
   Goptions.(declare_bool_option
     { optdepr  = false;
-      optname  = "suggest Proof using";
       optkey   = ["Suggest";"Proof";"Using"];
       optread  = (fun () -> !suggest_proof_using);
       optwrite = ((:=) suggest_proof_using) })
@@ -176,7 +175,6 @@ let proof_using_opt_name = ["Default";"Proof";"Using"]
 let () =
   Goptions.(declare_stringopt_option
     { optdepr  = false;
-      optname  = "default value for Proof using";
       optkey   = proof_using_opt_name;
       optread  = (fun () -> Option.map using_to_string !value);
       optwrite = (fun b -> value := Option.map using_from_string b);
-- 
cgit v1.2.3