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 -
 1 file changed, 1 deletion(-)

(limited to 'plugins/rtauto/proof_search.ml')

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)}
-- 
cgit v1.2.3