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

(limited to 'engine/namegen.ml')

diff --git a/engine/namegen.ml b/engine/namegen.ml
index 56277e8092..bcc8c34a4d 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -216,7 +216,6 @@ let it_mkLambda_or_LetIn_name env sigma b hyps =
 let get_mangle_names =
   Goptions.declare_bool_option_and_ref
     ~depr:false
-    ~name:"mangle auto-generated names"
     ~key:["Mangle";"Names"]
     ~value:false
 
@@ -227,7 +226,6 @@ let set_prefix x = mangle_names_prefix := forget_subscript x
 let () = Goptions.(
     declare_string_option
       { optdepr  = false;
-        optname  = "mangled names prefix";
         optkey   = ["Mangle";"Names";"Prefix"];
         optread  = (fun () -> Id.to_string !mangle_names_prefix);
         optwrite = begin fun x ->
-- 
cgit v1.2.3