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.
---
 pretyping/reductionops.ml | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'pretyping/reductionops.ml')

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index d5beebe690..bfee07e7f0 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -32,8 +32,6 @@ exception Elimconst
 
 let () = Goptions.(declare_bool_option {
   optdepr = false;
-  optname =
-    "Generate weak constraints between Irrelevant universes";
   optkey = ["Cumulativity";"Weak";"Constraints"];
   optread = (fun () -> not !UState.drop_weak_constraints);
   optwrite = (fun a -> UState.drop_weak_constraints:=not a);
@@ -972,8 +970,6 @@ module CredNative = RedNative(CNativeEntries)
 let debug_RAKAM = ref (false)
 let () = Goptions.(declare_bool_option {
   optdepr = false;
-  optname =
-    "Print states of the Reductionops abstract machine";
   optkey = ["Debug";"RAKAM"];
   optread = (fun () -> !debug_RAKAM);
   optwrite = (fun a -> debug_RAKAM:=a);
-- 
cgit v1.2.3