diff options
| author | Gaëtan Gilbert | 2019-04-01 13:44:54 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-04-12 13:59:23 +0200 |
| commit | 839ed4e80ca4dc068422c7c9fdb0c00e4ff1ebab (patch) | |
| tree | 37a4e9a4b9d291d630f63eb37f7307f91fe65d60 /vernac/proof_using.ml | |
| parent | 38b86f40b3e2c6ce0ea77c94cf0c48efbf7c9f13 (diff) | |
Unify Set and Unset handling for options
Not sure if the idetop.set_options was correctly changed, ocaml types
pass at least.
Diffstat (limited to 'vernac/proof_using.ml')
| -rw-r--r-- | vernac/proof_using.ml | 3 |
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); }) |