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.
---
 user-contrib/Ltac2/tac2entries.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'user-contrib')

diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index bcc5f54505..d6db4a735c 100644
--- a/user-contrib/Ltac2/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
@@ -824,7 +824,6 @@ let register_struct ?local str = match str with
 
 let _ = Goptions.declare_bool_option {
   Goptions.optdepr = false;
-  Goptions.optname = "print Ltac2 backtrace";
   Goptions.optkey = ["Ltac2"; "Backtrace"];
   Goptions.optread = (fun () -> !Tac2interp.print_ltac2_backtrace);
   Goptions.optwrite = (fun b -> Tac2interp.print_ltac2_backtrace := b);
-- 
cgit v1.2.3