Merge PR #9876: Command-line setters for options

Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: gares

1 files changed, 2 insertions, 1 deletions

diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml
index 526845084a..1d089d0a55 100644
--- a/vernac/proof_using.ml
+++ b/vernac/proof_using.ml
@@ -172,11 +172,12 @@ let value = ref None
 let using_to_string us = Pp.string_of_ppcmds (Ppvernac.pr_using us)
 let using_from_string us = Pcoq.Entry.parse G_vernac.section_subset_expr (Pcoq.Parsable.make (Stream.of_string us))
 
+let proof_using_opt_name = ["Default";"Proof";"Using"]
 let () =
   Goptions.(declare_stringopt_option
     { optdepr  = false;
       optname  = "default value for Proof using";
-      optkey   = ["Default";"Proof";"Using"];
+      optkey   = proof_using_opt_name;
       optread  = (fun () -> Option.map using_to_string !value);
       optwrite = (fun b -> value := Option.map using_from_string b);
     })