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/program.ml | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'pretyping/program.ml')

diff --git a/pretyping/program.ml b/pretyping/program.ml
index 1bc31646dd..9c478844aa 100644
--- a/pretyping/program.ml
+++ b/pretyping/program.ml
@@ -78,7 +78,6 @@ open Goptions
 let () =
   declare_bool_option
   { optdepr  = false;
-    optname  = "preferred transparency of Program obligations";
     optkey   = ["Transparent";"Obligations"];
     optread  = get_proofs_transparency;
     optwrite = set_proofs_transparency; }
@@ -86,7 +85,6 @@ let () =
 let () =
   declare_bool_option
   { optdepr  = false;
-    optname  = "program cases";
     optkey   = ["Program";"Cases"];
     optread  = (fun () -> !program_cases);
     optwrite = (:=) program_cases }
@@ -94,7 +92,6 @@ let () =
 let () =
   declare_bool_option
   { optdepr  = false;
-    optname  = "program generalized coercion";
     optkey   = ["Program";"Generalized";"Coercion"];
     optread  = (fun () -> !program_generalized_coercion);
     optwrite = (:=) program_generalized_coercion }
-- 
cgit v1.2.3