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`.

1 files changed, 4 insertions, 3 deletions

diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 5723b47715..254f772ff8 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -29,11 +29,12 @@ val print_evar_arguments : bool ref
 
 (** If true, contract branches with same r.h.s. and same matching
     variables in a disjunctive pattern *)
-val print_factorize_match_patterns : bool ref
+val print_factorize_match_patterns : unit -> bool
 
-(** If true and the last non unique clause of a "match" is a
+(** If this flag is true and the last non unique clause of a "match" is a
     variable-free disjunctive pattern, turn it into a catch-call case *)
-val print_allow_match_default_clause : bool ref
+val print_allow_match_default_clause : unit -> bool
+val print_allow_match_default_opt_name : string list
 
 val subst_cases_pattern : substitution -> cases_pattern -> cases_pattern