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

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index 4c539684e3..5402600041 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2849,7 +2849,6 @@ let process_back_meta_command ~newtip ~head oid aast =
 let get_allow_nested_proofs =
   Goptions.declare_bool_option_and_ref
     ~depr:false
-    ~name:"Nested Proofs Allowed"
     ~key:Vernac_classifier.stm_allow_nested_proofs_option_name
     ~value:false
 
-- 
cgit v1.2.3