aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/cc/ccalgo.ml2
-rw-r--r--plugins/extraction/table.ml8
-rw-r--r--plugins/firstorder/g_ground.ml44
-rw-r--r--plugins/funind/indfun_common.ml4
-rw-r--r--plugins/interface/xlate.ml28
-rw-r--r--plugins/omega/coq_omega.ml6
-rw-r--r--plugins/rtauto/proof_search.ml2
-rw-r--r--plugins/rtauto/refl_tauto.ml4
-rw-r--r--plugins/subtac/subtac_obligations.ml2
9 files changed, 30 insertions, 30 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 2d7dd9d6c..418980c54 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -31,7 +31,7 @@ let _=
let gdopt=
{ optsync=true;
optname="Congruence Verbose";
- optkey=SecondaryTable("Congruence","Verbose");
+ optkey=["Congruence";"Verbose"];
optread=(fun ()-> !cc_verbose);
optwrite=(fun b -> cc_verbose := b)}
in
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index f1e8f42fe..83a780198 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -327,7 +327,7 @@ let auto_inline () = !auto_inline_ref
let _ = declare_bool_option
{optsync = true;
optname = "Extraction AutoInline";
- optkey = SecondaryTable ("Extraction", "AutoInline");
+ optkey = ["Extraction"; "AutoInline"];
optread = auto_inline;
optwrite = (:=) auto_inline_ref}
@@ -340,7 +340,7 @@ let type_expand () = !type_expand_ref
let _ = declare_bool_option
{optsync = true;
optname = "Extraction TypeExpand";
- optkey = SecondaryTable ("Extraction", "TypeExpand");
+ optkey = ["Extraction"; "TypeExpand"];
optread = type_expand;
optwrite = (:=) type_expand_ref}
@@ -389,14 +389,14 @@ let optims () = !opt_flag_ref
let _ = declare_bool_option
{optsync = true;
optname = "Extraction Optimize";
- optkey = SecondaryTable ("Extraction", "Optimize");
+ optkey = ["Extraction"; "Optimize"];
optread = (fun () -> !int_flag_ref <> 0);
optwrite = (fun b -> chg_flag (if b then int_flag_init else 0))}
let _ = declare_int_option
{ optsync = true;
optname = "Extraction Flag";
- optkey = SecondaryTable("Extraction","Flag");
+ optkey = ["Extraction";"Flag"];
optread = (fun _ -> Some !int_flag_ref);
optwrite = (function
| None -> chg_flag 0
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index d7c5b66ae..96c5bcae4 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -30,7 +30,7 @@ let _=
let gdopt=
{ optsync=true;
optname="Firstorder Depth";
- optkey=SecondaryTable("Firstorder","Depth");
+ optkey=["Firstorder";"Depth"];
optread=(fun ()->Some !ground_depth);
optwrite=
(function
@@ -45,7 +45,7 @@ let _=
let gdopt=
{ optsync=true;
optname="Congruence Depth";
- optkey=SecondaryTable("Congruence","Depth");
+ optkey=["Congruence";"Depth"];
optread=(fun ()->Some !congruence_depth);
optwrite=
(function
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 69cc0607b..b29bdf3f1 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -495,7 +495,7 @@ let function_debug_sig =
{
optsync = false;
optname = "Function debug";
- optkey = PrimaryTable("Function_debug");
+ optkey = ["Function_debug"];
optread = (fun () -> !function_debug);
optwrite = (fun b -> function_debug := b)
}
@@ -514,7 +514,7 @@ let strict_tcc_sig =
{
optsync = false;
optname = "Raw Function Tcc";
- optkey = PrimaryTable("Function_raw_tcc");
+ optkey = ["Function_raw_tcc"];
optread = (fun () -> !strict_tcc);
optwrite = (fun b -> strict_tcc := b)
}
diff --git a/plugins/interface/xlate.ml b/plugins/interface/xlate.ml
index 6f9e673a9..bff8cae26 100644
--- a/plugins/interface/xlate.ml
+++ b/plugins/interface/xlate.ml
@@ -404,7 +404,7 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
| CPrim (_, String _) -> xlate_error "CPrim (String): TODO"
| CHole _ -> CT_existvarc
(* I assume CDynamic has been inserted to make free form extension of
- the language possible, but this would go agains the logic of pcoq anyway. *)
+ the language possible, but this would go against the logic of pcoq anyway. *)
| CDynamic (_, _) -> assert false
| CDelimiters (_, key, num) ->
CT_num_encapsulator(CT_num_type key , xlate_formula num)
@@ -2179,21 +2179,21 @@ let rec xlate_vernac =
| VernacLocate(LocateNotation s) -> CT_locate_notation(CT_string s)
| VernacTime(v) -> CT_time(xlate_vernac v)
| VernacTimeout(n,v) -> CT_timeout(CT_int n,xlate_vernac v)
- | VernacSetOption (Goptions.SecondaryTable ("Implicit", "Arguments"), BoolValue true)->CT_user_vernac (CT_ident "IMPLICIT_ARGS_ON", CT_varg_list[])
+ | VernacSetOption (["Implicit"; "Arguments"], BoolValue true)->CT_user_vernac (CT_ident "IMPLICIT_ARGS_ON", CT_varg_list[])
|VernacExactProof f -> CT_proof(xlate_formula f)
| VernacSetOption (table, BoolValue true) ->
let table1 =
match table with
- PrimaryTable(s) -> CT_coerce_ID_to_TABLE(CT_ident s)
- | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2)
- | TertiaryTable(s1,s2,s3) -> xlate_error "TODO: TertiaryTable" in
+ [s] -> CT_coerce_ID_to_TABLE(CT_ident s)
+ | [s1;s2] -> CT_table(CT_ident s1, CT_ident s2)
+ | _ -> xlate_error "TODO: arbitrary-length Table names" in
CT_set_option(table1)
| VernacSetOption (table, v) ->
let table1 =
match table with
- PrimaryTable(s) -> CT_coerce_ID_to_TABLE(CT_ident s)
- | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2)
- | TertiaryTable(s1,s2,s3) -> xlate_error "TODO: TertiaryTable" in
+ [s] -> CT_coerce_ID_to_TABLE(CT_ident s)
+ | [s1;s2] -> CT_table(CT_ident s1, CT_ident s2)
+ | _ -> xlate_error "TODO: arbitrary-length Table names" in
let value =
match v with
| BoolValue _ -> assert false
@@ -2205,9 +2205,9 @@ let rec xlate_vernac =
| VernacUnsetOption(table) ->
let table1 =
match table with
- PrimaryTable(s) -> CT_coerce_ID_to_TABLE(CT_ident s)
- | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2)
- | TertiaryTable(s1,s2,s3) -> xlate_error "TODO: TertiaryTable" in
+ [s] -> CT_coerce_ID_to_TABLE(CT_ident s)
+ | [s1;s2] -> CT_table(CT_ident s1, CT_ident s2)
+ | _ -> xlate_error "TODO: arbitrary-length Table names" in
CT_unset_option(table1)
| VernacAddOption (table, l) ->
let values =
@@ -2221,9 +2221,9 @@ let rec xlate_vernac =
match values with [] -> assert false | a::b -> (a,b) in
let table1 =
match table with
- PrimaryTable(s) -> CT_coerce_ID_to_TABLE(CT_ident s)
- | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2)
- | TertiaryTable(s1,s2,s3) -> xlate_error "TODO: TertiaryTable" in
+ [s] -> CT_coerce_ID_to_TABLE(CT_ident s)
+ | [s1;s2] -> CT_table(CT_ident s1, CT_ident s2)
+ | _ -> xlate_error "TODO: arbitrary-length Table names" in
CT_set_option_value2(table1, CT_id_or_string_ne_list(fst, values1))
| VernacImport(true, a::l) ->
CT_export_id(CT_id_ne_list(reference_to_ct_ID a,
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 535459885..8c8640ea5 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -61,7 +61,7 @@ let _ =
declare_bool_option
{ optsync = false;
optname = "Omega system time displaying flag";
- optkey = SecondaryTable ("Omega","System");
+ optkey = ["Omega";"System"];
optread = read display_system_flag;
optwrite = write display_system_flag }
@@ -69,7 +69,7 @@ let _ =
declare_bool_option
{ optsync = false;
optname = "Omega action display flag";
- optkey = SecondaryTable ("Omega","Action");
+ optkey = ["Omega";"Action"];
optread = read display_action_flag;
optwrite = write display_action_flag }
@@ -77,7 +77,7 @@ let _ =
declare_bool_option
{ optsync = false;
optname = "Omega old style flag";
- optkey = SecondaryTable ("Omega","OldStyle");
+ optkey = ["Omega";"OldStyle"];
optread = read old_style_flag;
optwrite = write old_style_flag }
diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml
index 9d9d66bb2..1fee72a60 100644
--- a/plugins/rtauto/proof_search.ml
+++ b/plugins/rtauto/proof_search.ml
@@ -50,7 +50,7 @@ let pruning = ref true
let opt_pruning=
{optsync=true;
optname="Rtauto Pruning";
- optkey=SecondaryTable("Rtauto","Pruning");
+ optkey=["Rtauto";"Pruning"];
optread=(fun () -> !pruning);
optwrite=(fun b -> pruning:=b)}
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 6cde1ddcf..b47bbaa93 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -245,7 +245,7 @@ let verbose = ref false
let opt_verbose=
{optsync=true;
optname="Rtauto Verbose";
- optkey=SecondaryTable("Rtauto","Verbose");
+ optkey=["Rtauto";"Verbose"];
optread=(fun () -> !verbose);
optwrite=(fun b -> verbose:=b)}
@@ -256,7 +256,7 @@ let check = ref false
let opt_check=
{optsync=true;
optname="Rtauto Check";
- optkey=SecondaryTable("Rtauto","Check");
+ optkey=["Rtauto";"Check"];
optread=(fun () -> !check);
optwrite=(fun b -> check:=b)}
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index a54b3a86f..a8f5815bc 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -77,7 +77,7 @@ let _ =
declare_bool_option
{ optsync = true;
optname = "transparency of Program obligations";
- optkey = (SecondaryTable ("Transparent","Obligations"));
+ optkey = ["Transparent";"Obligations"];
optread = get_proofs_transparency;
optwrite = set_proofs_transparency; }
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 11:19:14 +0000