aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--ide/idetop.ml17
-rw-r--r--plugins/ssr/ssrvernac.mlg2
-rw-r--r--stm/vernac_classifier.ml8
-rw-r--r--toplevel/coqloop.ml4
-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
10 files changed, 46 insertions, 63 deletions
diff --git a/ide/idetop.ml b/ide/idetop.ml
index 10b8a2cdc5..543ff924bd 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -57,9 +57,9 @@ let coqide_known_option table = List.mem table [
["Diffs"]]
let is_known_option cmd = match Vernacprop.under_control cmd with
- | VernacSetOption (_, o, BoolValue true)
- | VernacSetOption (_, o, StringValue _)
- | VernacUnsetOption (_, o) -> coqide_known_option o
+ | VernacSetOption (_, o, OptionSetTrue)
+ | VernacSetOption (_, o, OptionSetString _)
+ | VernacSetOption (_, o, OptionUnset) -> coqide_known_option o
| _ -> false
(** Check whether a command is forbidden in the IDE *)
@@ -366,12 +366,13 @@ let get_options () =
Goptions.OptionMap.fold fold table []
let set_options options =
+ let open Goptions in
let iter (name, value) = match import_option_value value with
- | BoolValue b -> Goptions.set_bool_option_value name b
- | IntValue i -> Goptions.set_int_option_value name i
- | StringValue s -> Goptions.set_string_option_value name s
- | StringOptValue (Some s) -> Goptions.set_string_option_value name s
- | StringOptValue None -> Goptions.unset_option_value_gen name
+ | BoolValue b -> set_bool_option_value name b
+ | IntValue i -> set_int_option_value name i
+ | StringValue s -> set_string_option_value name s
+ | StringOptValue (Some s) -> set_string_option_value name s
+ | StringOptValue None -> unset_option_value_gen name
in
List.iter iter options
diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index 0a0d9b12fa..bf7f082192 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -183,7 +183,7 @@ GRAMMAR EXTEND Gram
GLOBAL: gallina_ext;
gallina_ext:
[ [ IDENT "Import"; IDENT "Prenex"; IDENT "Implicits" ->
- { Vernacexpr.VernacUnsetOption (false, ["Printing"; "Implicit"; "Defensive"]) }
+ { Vernacexpr.VernacSetOption (false, ["Printing"; "Implicit"; "Defensive"], Vernacexpr.OptionUnset) }
] ]
;
END
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 58fe923f9e..243b5c333d 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -57,6 +57,7 @@ let options_affecting_stm_scheduling =
stm_allow_nested_proofs_option_name;
Vernacentries.proof_mode_opt_name;
Attributes.program_mode_option_name;
+ Proof_using.proof_using_opt_name;
]
let classify_vernac e =
@@ -64,7 +65,7 @@ let classify_vernac e =
(* Univ poly compatibility: we run it now, so that we can just
* look at Flags in stm.ml. Would be nicer to have the stm
* look at the entire dag to detect this option. *)
- | ( VernacSetOption (_, l,_) | VernacUnsetOption (_, l))
+ | VernacSetOption (_, l,_)
when CList.exists (CList.equal String.equal l)
options_affecting_stm_scheduling ->
VtSideff [], VtNow
@@ -91,9 +92,6 @@ let classify_vernac e =
VtProofStep { parallel = `No;
proof_block_detection = Some "curly" },
VtLater
- (* Options changing parser *)
- | VernacUnsetOption (_, ["Default";"Proof";"Using"])
- | VernacSetOption (_, ["Default";"Proof";"Using"],_) -> VtSideff [], VtNow
(* StartProof *)
| VernacDefinition ((Decl_kinds.DoDischarge,_),({v=i},_),ProveBody _) ->
VtStartProof(Doesn'tGuaranteeOpacity, idents_of_name i), VtLater
@@ -156,7 +154,7 @@ let classify_vernac e =
| VernacReserve _
| VernacGeneralizable _
| VernacSetOpacity _ | VernacSetStrategy _
- | VernacUnsetOption _ | VernacSetOption _
+ | VernacSetOption _
| VernacAddOption _ | VernacRemoveOption _
| VernacMemOption _ | VernacPrintOption _
| VernacGlobalCheck _
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index b3de8dd85f..4129562065 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -340,9 +340,7 @@ let print_anyway_opts = [
let print_anyway c =
let open Vernacexpr in
match c with
- | VernacExpr (_, VernacSetOption (_, opt, _))
- | VernacExpr (_, VernacUnsetOption (_, opt)) ->
- List.mem opt print_anyway_opts
+ | VernacExpr (_, VernacSetOption (_, opt, _)) -> List.mem opt print_anyway_opts
| _ -> false
(* We try to behave better when goal printing raises an exception
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 19:02:47 +0000