aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/cc/ccalgo.ml3
-rw-r--r--plugins/extraction/table.ml15
-rw-r--r--plugins/firstorder/g_ground.ml46
-rw-r--r--plugins/funind/indfun_common.ml3
-rw-r--r--plugins/ltac/g_ltac.ml41
-rw-r--r--plugins/ltac/profile_ltac.ml3
-rw-r--r--plugins/ltac/tacinterp.ml6
-rw-r--r--plugins/ltac/tactic_debug.ml3
-rw-r--r--plugins/ltac/tauto.ml6
-rw-r--r--plugins/micromega/coq_micromega.ml2
-rw-r--r--plugins/omega/coq_omega.ml12
-rw-r--r--plugins/rtauto/proof_search.ml3
-rw-r--r--plugins/rtauto/refl_tauto.ml6
-rw-r--r--plugins/ssrmatching/ssrmatching.ml46
14 files changed, 23 insertions, 52 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index aa71a4565..5dea4631c 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -29,8 +29,7 @@ let debug x =
let _=
let gdopt=
- { optsync=true;
- optdepr=false;
+ { optdepr=false;
optname="Congruence Verbose";
optkey=["Congruence";"Verbose"];
optread=(fun ()-> !cc_verbose);
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 0cdb10a37..fc1ed335a 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -494,8 +494,7 @@ let my_bool_option name initval =
let flag = ref initval in
let access = fun () -> !flag in
let _ = declare_bool_option
- {optsync = true;
- optdepr = false;
+ {optdepr = false;
optname = "Extraction "^name;
optkey = ["Extraction"; name];
optread = access;
@@ -567,16 +566,14 @@ let chg_flag n = int_flag_ref := n; opt_flag_ref := flag_of_int n
let optims () = !opt_flag_ref
let _ = declare_bool_option
- {optsync = true;
- optdepr = false;
+ {optdepr = false;
optname = "Extraction Optimize";
optkey = ["Extraction"; "Optimize"];
optread = (fun () -> not (Int.equal !int_flag_ref 0));
optwrite = (fun b -> chg_flag (if b then int_flag_init else 0))}
let _ = declare_int_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "Extraction Flag";
optkey = ["Extraction";"Flag"];
optread = (fun _ -> Some !int_flag_ref);
@@ -590,8 +587,7 @@ let conservative_types_ref = ref false
let conservative_types () = !conservative_types_ref
let _ = declare_bool_option
- {optsync = true;
- optdepr = false;
+ {optdepr = false;
optname = "Extraction Conservative Types";
optkey = ["Extraction"; "Conservative"; "Types"];
optread = (fun () -> !conservative_types_ref);
@@ -603,8 +599,7 @@ let file_comment_ref = ref ""
let file_comment () = !file_comment_ref
let _ = declare_string_option
- {optsync = true;
- optdepr = false;
+ {optdepr = false;
optname = "Extraction File Comment";
optkey = ["Extraction"; "File"; "Comment"];
optread = (fun () -> !file_comment_ref);
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 90e5f3ca5..bbb9feae2 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -30,8 +30,7 @@ let ground_depth=ref 3
let _=
let gdopt=
- { optsync=true;
- optdepr=false;
+ { optdepr=false;
optname="Firstorder Depth";
optkey=["Firstorder";"Depth"];
optread=(fun ()->Some !ground_depth);
@@ -46,8 +45,7 @@ let congruence_depth=ref 100
let _=
let gdopt=
- { optsync=true;
- optdepr=false;
+ { optdepr=false;
optname="Congruence Depth";
optkey=["Congruence";"Depth"];
optread=(fun ()->Some !congruence_depth);
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 8ec3d9b3e..ea985ddec 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -422,7 +422,6 @@ open Goptions
let functional_induction_rewrite_dependent_proofs_sig =
{
- optsync = false;
optdepr = false;
optname = "Functional Induction Rewrite Dependent";
optkey = ["Functional";"Induction";"Rewrite";"Dependent"];
@@ -435,7 +434,6 @@ let do_rewrite_dependent () = !functional_induction_rewrite_dependent_proofs = t
let function_debug_sig =
{
- optsync = false;
optdepr = false;
optname = "Function debug";
optkey = ["Function_debug"];
@@ -454,7 +452,6 @@ let strict_tcc = ref false
let is_strict_tcc () = !strict_tcc
let strict_tcc_sig =
{
- optsync = false;
optdepr = false;
optname = "Raw Function Tcc";
optkey = ["Function_raw_tcc"];
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index b5028190f..36ac10bfe 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -367,7 +367,6 @@ open Libnames
let print_info_trace = ref None
let _ = declare_int_option {
- optsync = true;
optdepr = false;
optname = "print info trace";
optkey = ["Info" ; "Level"];
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index c5dbc8a14..3ff7b53c7 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -411,8 +411,7 @@ let _ = Declaremods.append_end_library_hook do_print_results_at_close
let _ =
let open Goptions in
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "Ltac Profiling";
optkey = ["Ltac"; "Profiling"];
optread = get_profiling;
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index f63c38d4f..8a10a4d76 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -2136,8 +2136,7 @@ let vernac_debug b =
let _ =
let open Goptions in
declare_bool_option
- { optsync = false;
- optdepr = false;
+ { optdepr = false;
optname = "Ltac debug";
optkey = ["Ltac";"Debug"];
optread = (fun () -> get_debug () != Tactic_debug.DebugOff);
@@ -2146,8 +2145,7 @@ let _ =
let _ =
let open Goptions in
declare_bool_option
- { optsync = false;
- optdepr = false;
+ { optdepr = false;
optname = "Ltac debug";
optkey = ["Debug";"Ltac"];
optread = (fun () -> get_debug () != Tactic_debug.DebugOff);
diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index 20a2013a5..294cba4d7 100644
--- a/plugins/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
@@ -91,8 +91,7 @@ open Goptions
let _ =
declare_bool_option
- { optsync = false;
- optdepr = false;
+ { optdepr = false;
optname = "Ltac batch debug";
optkey = ["Ltac";"Batch";"Debug"];
optread = (fun () -> !batch);
diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml
index 1e46c253d..4ec111e01 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -70,8 +70,7 @@ let unfold_iff () = !iff_unfolding || Flags.version_less_or_equal Flags.V8_2
open Goptions
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "unfolding of not in intuition";
optkey = ["Intuition";"Negation";"Unfolding"];
optread = (fun () -> !negation_unfolding);
@@ -79,8 +78,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "unfolding of iff in intuition";
optkey = ["Intuition";"Iff";"Unfolding"];
optread = (fun () -> !iff_unfolding);
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index b6ad784d9..053bb6fa1 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -65,7 +65,6 @@ let _ =
let int_opt l vref =
{
- optsync = true;
optdepr = false;
optname = List.fold_right (^) l "";
optkey = l ;
@@ -75,7 +74,6 @@ let _ =
let lia_enum_opt =
{
- optsync = true;
optdepr = false;
optname = "Lia Enum";
optkey = ["Lia";"Enum"];
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 92b092ffe..334baec8d 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -71,8 +71,7 @@ open Goptions
let _ =
declare_bool_option
- { optsync = false;
- optdepr = false;
+ { optdepr = false;
optname = "Omega system time displaying flag";
optkey = ["Omega";"System"];
optread = read display_system_flag;
@@ -80,8 +79,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = false;
- optdepr = false;
+ { optdepr = false;
optname = "Omega action display flag";
optkey = ["Omega";"Action"];
optread = read display_action_flag;
@@ -89,8 +87,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = false;
- optdepr = false;
+ { optdepr = false;
optname = "Omega old style flag";
optkey = ["Omega";"OldStyle"];
optread = read old_style_flag;
@@ -98,8 +95,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = true;
+ { optdepr = true;
optname = "Omega automatic reset of generated names";
optkey = ["Stable";"Omega"];
optread = read reset_flag;
diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml
index 1ad4d622b..4eef1b0a7 100644
--- a/plugins/rtauto/proof_search.ml
+++ b/plugins/rtauto/proof_search.ml
@@ -46,8 +46,7 @@ let reset_info () =
let pruning = ref true
let opt_pruning=
- {optsync=true;
- optdepr=false;
+ {optdepr=false;
optname="Rtauto Pruning";
optkey=["Rtauto";"Pruning"];
optread=(fun () -> !pruning);
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 3655df895..d580fde29 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -236,8 +236,7 @@ open Goptions
let verbose = ref false
let opt_verbose=
- {optsync=true;
- optdepr=false;
+ {optdepr=false;
optname="Rtauto Verbose";
optkey=["Rtauto";"Verbose"];
optread=(fun () -> !verbose);
@@ -248,8 +247,7 @@ let _ = declare_bool_option opt_verbose
let check = ref false
let opt_check=
- {optsync=true;
- optdepr=false;
+ {optdepr=false;
optname="Rtauto Check";
optkey=["Rtauto";"Check"];
optread=(fun () -> !check);
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index 8be060e19..862e44cca 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -63,8 +63,7 @@ let debug b =
if b then pp_ref := ssr_pp else pp_ref := fun _ -> ()
let _ =
Goptions.declare_bool_option
- { Goptions.optsync = false;
- Goptions.optname = "ssrmatching debugging";
+ { Goptions.optname = "ssrmatching debugging";
Goptions.optkey = ["Debug";"SsrMatching"];
Goptions.optdepr = false;
Goptions.optread = (fun _ -> !pp_ref == ssr_pp);
@@ -183,8 +182,7 @@ let profile b =
;;
let _ =
Goptions.declare_bool_option
- { Goptions.optsync = false;
- Goptions.optname = "ssrmatching profiling";
+ { Goptions.optname = "ssrmatching profiling";
Goptions.optkey = ["SsrMatchingProfiling"];
Goptions.optread = (fun _ -> !profile_now);
Goptions.optdepr = false;
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-03 19:21:31 +0000