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.
---
 engine/uState.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'engine/uState.ml')

diff --git a/engine/uState.ml b/engine/uState.ml
index 3546ece581..2eaa202246 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -53,7 +53,7 @@ let empty =
     uctx_weak_constraints = UPairSet.empty; }
 
 let elaboration_sprop_cumul =
-  Goptions.declare_bool_option_and_ref ~depr:false ~name:"SProp cumulativity during elaboration"
+  Goptions.declare_bool_option_and_ref ~depr:false
     ~key:["Elaboration";"StrictProp";"Cumulativity"] ~value:true
 
 let make ~lbound u =
-- 
cgit v1.2.3