aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/g_vernac.mlg20
-rw-r--r--vernac/ppvernac.ml21
-rw-r--r--vernac/proof_using.ml3
-rw-r--r--vernac/proof_using.mli3
-rw-r--r--vernac/vernacentries.ml18
-rw-r--r--vernac/vernacexpr.ml13
6 files changed, 32 insertions, 46 deletions
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 1533d0ccd3..3f491d1dd4 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -875,10 +875,10 @@ GRAMMAR EXTEND Gram
GLOBAL: command query_command class_rawexpr gallina_ext;
gallina_ext:
- [ [ IDENT "Export"; "Set"; table = option_table; v = option_value ->
+ [ [ IDENT "Export"; "Set"; table = option_table; v = option_setting ->
{ VernacSetOption (true, table, v) }
| IDENT "Export"; IDENT "Unset"; table = option_table ->
- { VernacUnsetOption (true, table) }
+ { VernacSetOption (true, table, OptionUnset) }
] ];
command:
@@ -943,10 +943,10 @@ GRAMMAR EXTEND Gram
{ VernacAddMLPath (true, dir) }
(* For acting on parameter tables *)
- | "Set"; table = option_table; v = option_value ->
+ | "Set"; table = option_table; v = option_setting ->
{ VernacSetOption (false, table, v) }
| IDENT "Unset"; table = option_table ->
- { VernacUnsetOption (false, table) }
+ { VernacSetOption (false, table, OptionUnset) }
| IDENT "Print"; IDENT "Table"; table = option_table ->
{ VernacPrintOption table }
@@ -1057,10 +1057,10 @@ GRAMMAR EXTEND Gram
| IDENT "Library"; qid = global -> { LocateLibrary qid }
| IDENT "Module"; qid = global -> { LocateModule qid } ] ]
;
- option_value:
- [ [ -> { BoolValue true }
- | n = integer -> { IntValue (Some n) }
- | s = STRING -> { StringValue s } ] ]
+ option_setting:
+ [ [ -> { OptionSetTrue }
+ | n = integer -> { OptionSetInt n }
+ | s = STRING -> { OptionSetString s } ] ]
;
option_ref_value:
[ [ id = global -> { QualidRefValue id }
@@ -1130,10 +1130,10 @@ GRAMMAR EXTEND Gram
(* Tactic Debugger *)
| IDENT "Debug"; IDENT "On" ->
- { VernacSetOption (false, ["Ltac";"Debug"], BoolValue true) }
+ { VernacSetOption (false, ["Ltac";"Debug"], OptionSetTrue) }
| IDENT "Debug"; IDENT "Off" ->
- { VernacSetOption (false, ["Ltac";"Debug"], BoolValue false) }
+ { VernacSetOption (false, ["Ltac";"Debug"], OptionUnset) }
(* registration of a custom reduction *)
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index b602e134da..4e4d431e89 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -173,15 +173,10 @@ open Pputils
pr_opt (prlist_with_sep sep pr_option_ref_value) b
let pr_set_option a b =
- let pr_opt_value = function
- | IntValue None -> assert false
- (* This should not happen because of the grammar *)
- | IntValue (Some n) -> spc() ++ int n
- | StringValue s -> spc() ++ str s
- | StringOptValue None -> mt()
- | StringOptValue (Some s) -> spc() ++ str s
- | BoolValue b -> mt()
- in pr_printoption a None ++ pr_opt_value b
+ pr_printoption a None ++ (match b with
+ | OptionUnset | OptionSetTrue -> mt()
+ | OptionSetInt n -> spc() ++ int n
+ | OptionSetString s -> spc() ++ quote (str s))
let pr_opt_hintbases l = match l with
| [] -> mt()
@@ -1140,15 +1135,11 @@ open Pputils
hov 1 (keyword "Strategy" ++ spc() ++
hv 0 (prlist_with_sep sep pr_line l))
)
- | VernacUnsetOption (export, na) ->
- let export = if export then keyword "Export" ++ spc () else mt () in
- return (
- hov 1 (export ++ keyword "Unset" ++ spc() ++ pr_printoption na None)
- )
| VernacSetOption (export, na,v) ->
let export = if export then keyword "Export" ++ spc () else mt () in
+ let set = if v == OptionUnset then "Unset" else "Set" in
return (
- hov 2 (export ++ keyword "Set" ++ spc() ++ pr_set_option na v)
+ hov 2 (export ++ keyword set ++ spc() ++ pr_set_option na v)
)
| VernacAddOption (na,l) ->
return (
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);
})
diff --git a/vernac/proof_using.mli b/vernac/proof_using.mli
index 7d1110aaa2..702043a4a9 100644
--- a/vernac/proof_using.mli
+++ b/vernac/proof_using.mli
@@ -21,3 +21,6 @@ val suggest_constant : Environ.env -> Names.Constant.t -> unit
val suggest_variable : Environ.env -> Names.Id.t -> unit
val get_default_proof_using : unit -> Vernacexpr.section_subset_expr option
+
+val proof_using_opt_name : string list
+(** For the stm *)
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 6c24b9ec75..3a305c3b61 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1707,18 +1707,17 @@ let get_option_locality export local =
let vernac_set_option0 ~local export key opt =
let locality = get_option_locality export local in
match opt with
- | StringValue s -> set_string_option_value_gen ~locality key s
- | StringOptValue (Some s) -> set_string_option_value_gen ~locality key s
- | StringOptValue None -> unset_option_value_gen ~locality key
- | IntValue n -> set_int_option_value_gen ~locality key n
- | BoolValue b -> set_bool_option_value_gen ~locality key b
+ | OptionUnset -> unset_option_value_gen ~locality key
+ | OptionSetString s -> set_string_option_value_gen ~locality key s
+ | OptionSetInt n -> set_int_option_value_gen ~locality key (Some n)
+ | OptionSetTrue -> set_bool_option_value_gen ~locality key true
let vernac_set_append_option ~local export key s =
let locality = get_option_locality export local in
set_string_option_append_value_gen ~locality key s
let vernac_set_option ~local export table v = match v with
-| StringValue s ->
+| OptionSetString s ->
(* We make a special case for warnings because appending is their
natural semantics *)
if CString.List.equal table ["Warnings"] then
@@ -1731,10 +1730,6 @@ let vernac_set_option ~local export table v = match v with
vernac_set_option0 ~local export table v
| _ -> vernac_set_option0 ~local export table v
-let vernac_unset_option ~local export key =
- let locality = get_option_locality export local in
- unset_option_value_gen ~locality key
-
let vernac_add_option key lv =
let f = function
| StringRefValue s -> (get_string_table key)#add s
@@ -2462,9 +2457,6 @@ let rec interp_expr ?proof ~atts ~st c : Proof_global.t option =
| VernacSetOption (export, key,v) ->
vernac_set_option ~local:(only_locality atts) export key v;
pstate
- | VernacUnsetOption (export, key) ->
- vernac_unset_option ~local:(only_locality atts) export key;
- pstate
| VernacRemoveOption (key,v) ->
unsupported_attributes atts;
vernac_remove_option key v;
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index ebfc473522..d5f4576ea2 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -109,11 +109,11 @@ type onlyparsing_flag = Flags.compat_version option
which this notation is trying to be compatible with *)
type locality_flag = bool (* true = Local *)
-type option_value = Goptions.option_value =
- | BoolValue of bool
- | IntValue of int option
- | StringValue of string
- | StringOptValue of string option
+type option_setting =
+ | OptionUnset
+ | OptionSetTrue
+ | OptionSetInt of int
+ | OptionSetString of string
type option_ref_value =
| StringRefValue of string
@@ -363,8 +363,7 @@ type nonrec vernac_expr =
| VernacSetOpacity of (Conv_oracle.level * qualid or_by_notation list)
| VernacSetStrategy of
(Conv_oracle.level * qualid or_by_notation list) list
- | VernacUnsetOption of export_flag * Goptions.option_name
- | VernacSetOption of export_flag * Goptions.option_name * option_value
+ | VernacSetOption of export_flag * Goptions.option_name * option_setting
| VernacAddOption of Goptions.option_name * option_ref_value list
| VernacRemoveOption of Goptions.option_name * option_ref_value list
| VernacMemOption of Goptions.option_name * option_ref_value list
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:41:43 +0000