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.
---
 plugins/rtauto/proof_search.ml | 1 -
 plugins/rtauto/refl_tauto.ml   | 2 --
 2 files changed, 3 deletions(-)

(limited to 'plugins/rtauto')

diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml
index 4cc32cfb26..ab34489de9 100644
--- a/plugins/rtauto/proof_search.ml
+++ b/plugins/rtauto/proof_search.ml
@@ -49,7 +49,6 @@ let pruning = ref true
 
 let opt_pruning=
   {optdepr=false;
-   optname="Rtauto Pruning";
    optkey=["Rtauto";"Pruning"];
    optread=(fun () -> !pruning);
    optwrite=(fun b -> pruning:=b)}
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 0c155c9d0a..b86c8d096c 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -227,7 +227,6 @@ let verbose = ref false
 
 let opt_verbose=
   {optdepr=false;
-   optname="Rtauto Verbose";
    optkey=["Rtauto";"Verbose"];
    optread=(fun () -> !verbose);
    optwrite=(fun b -> verbose:=b)}
@@ -238,7 +237,6 @@ let check = ref false
 
 let opt_check=
   {optdepr=false;
-   optname="Rtauto Check";
    optkey=["Rtauto";"Check"];
    optread=(fun () -> !check);
    optwrite=(fun b -> check:=b)}
-- 
cgit v1.2.3