From 5c5fbf68034fdd18ddfcd19c9c8b1438af6b5c92 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 1 Apr 2020 16:54:37 +0200
Subject: Clean and fix definitions of options.

- Provide new helper functions in `Goptions` on the model of
  `declare_bool_option_and_ref`;

- Use these helper functions in many parts of the code base
  (encapsulates the corresponding references);

- Move almost all options from `declare_string_option` to
  `declare_stringopt_option` (only "Warnings" continue to use the
  former).  This means that these options now support `Unset` to get
  back to the default setting.  Note that there is a naming
  misalignment since `declare_int_option` is similar to
  `declare_stringopt_option` and supports `Unset`.  When "Warning" is
  eventually migrated to support `Unset` as well, we can remove
  `declare_string_option` and rename `declare_stringopt_option` to
  `declare_string_option`.

- For some vernac options and flags that have an equivalent
  command-line option or flag, implement it like the standard `-set`
  and `-unset`.
---
 printing/proof_diffs.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'printing/proof_diffs.mli')

diff --git a/printing/proof_diffs.mli b/printing/proof_diffs.mli
index 24b171770a..ea64439456 100644
--- a/printing/proof_diffs.mli
+++ b/printing/proof_diffs.mli
@@ -10,8 +10,8 @@
 
 (* diff options *)
 
-(** Controls whether to show diffs.  Takes values "on", "off", "removed" *)
-val write_diffs_option : string -> unit
+(** Name of Diffs option *)
+val opt_name : string list
 
 (** Returns true if the diffs option is "on" or "removed" *)
 val show_diffs : unit -> bool
-- 
cgit v1.2.3