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/proof_diffs.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'printing/proof_diffs.ml')

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