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

(limited to 'plugins/cc')

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index fdc70ccaa8..f9078c4bdc 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -33,7 +33,6 @@ let debug x =
 let () =
   let gdopt=
     { optdepr=false;
-      optname="Congruence Verbose";
       optkey=["Congruence";"Verbose"];
       optread=(fun ()-> !cc_verbose);
       optwrite=(fun b -> cc_verbose := b)}
-- 
cgit v1.2.3