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.
---
 interp/constrextern.ml | 1 -
 interp/constrintern.ml | 1 -
 2 files changed, 2 deletions(-)

(limited to 'interp')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index c55e17e7a3..c198c4eb9b 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -194,7 +194,6 @@ let without_specific_symbols l =
 let get_record_print =
   Goptions.declare_bool_option_and_ref
     ~depr:false
-    ~name:"record printing"
     ~key:["Printing";"Records"]
     ~value:true
 
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 2ceea58297..b2c572d290 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1615,7 +1615,6 @@ let is_non_zero_pat c = match c with
 
 let get_asymmetric_patterns = Goptions.declare_bool_option_and_ref
     ~depr:false
-    ~name:"no parameters in constructors"
     ~key:["Asymmetric";"Patterns"]
     ~value:false
 
-- 
cgit v1.2.3