aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--dev/ci/ci-user-overlay.sh20
-rw-r--r--dev/doc/changes.txt7
-rw-r--r--engine/namegen.ml3
-rw-r--r--ide/ide_slave.ml2
-rw-r--r--interp/constrextern.ml3
-rw-r--r--interp/topconstr.ml2
-rw-r--r--library/goptions.ml47
-rw-r--r--library/goptions.mli11
-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
-rw-r--r--pretyping/cbv.ml2
-rw-r--r--pretyping/classops.ml4
-rw-r--r--pretyping/coercion.ml7
-rw-r--r--pretyping/detyping.ml15
-rw-r--r--pretyping/evarconv.ml2
-rw-r--r--pretyping/pretyping.ml6
-rw-r--r--pretyping/program.ml9
-rw-r--r--pretyping/reductionops.ml4
-rw-r--r--pretyping/typeclasses.ml3
-rw-r--r--pretyping/unification.ml10
-rw-r--r--printing/printer.ml15
-rw-r--r--printing/printmod.ml3
-rw-r--r--proofs/pfedit.ml2
-rw-r--r--proofs/proof_global.ml19
-rw-r--r--proofs/proof_using.ml6
-rw-r--r--proofs/redexpr.ml2
-rw-r--r--tactics/auto.ml3
-rw-r--r--tactics/class_tactics.ml30
-rw-r--r--tactics/eauto.ml6
-rw-r--r--tactics/equality.ml15
-rw-r--r--tactics/hints.ml3
-rw-r--r--tactics/tactics.ml20
-rw-r--r--vernac/classes.ml1
-rw-r--r--vernac/indschemes.ml24
-rw-r--r--vernac/lemmas.ml3
-rw-r--r--vernac/obligations.ml6
-rw-r--r--vernac/record.ml9
-rw-r--r--vernac/search.ml1
-rw-r--r--vernac/vernacentries.ml87
51 files changed, 156 insertions, 331 deletions
diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh
index 71d098e37..1f7fbcbf6 100644
--- a/dev/ci/ci-user-overlay.sh
+++ b/dev/ci/ci-user-overlay.sh
@@ -25,24 +25,8 @@ echo $TRAVIS_PULL_REQUEST
echo $TRAVIS_BRANCH
echo $TRAVIS_COMMIT
-if [ $TRAVIS_PULL_REQUEST == "402" ] || [ $TRAVIS_BRANCH == "located_switch" ]; then
-
- mathcomp_CI_BRANCH=located_switch
+if [ $TRAVIS_PULL_REQUEST == "481" ] || [ $TRAVIS_BRANCH == "options+remove_non_sync" ]; then
+ mathcomp_CI_BRANCH=options+remove_non_sync
mathcomp_CI_GITURL=https://github.com/ejgallego/math-comp.git
-
- fiat_parsers_CI_BRANCH=located_switch
- fiat_parsers_CI_GITURL=https://github.com/ejgallego/fiat.git
-
- bedrock_src_CI_BRANCH=located_switch
- bedrock_src_CI_GITURL=https://github.com/ejgallego/bedrock.git
-
- bedrock_facade_CI_BRANCH=located_switch
- bedrock_facade_CI_GITURL=https://github.com/ejgallego/bedrock.git
-
-fi
-
-if [ $TRAVIS_PULL_REQUEST == "406" ] || [ $TRAVIS_BRANCH == "feature/coq_makefile2" ]; then
- UniMath_CI_BRANCH=master
- UniMath_CI_GITURL=https://github.com/gares/UniMath.git
fi
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 527721f8a..a2ae8254d 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -101,6 +101,13 @@ type 'a ast = private {
implemented in the whole code base. Matching a located object hasn't
changed, however, `Loc.tag ?loc obj` must be used to build one.
+In GOption:
+
+ Support for non-synchronous options has been removed. Now all
+ options are handled as a piece of normal document state, and thus
+ passed to workers, etc... As a consequence, the field
+ `Goptions.optsync` has been removed.
+
** Tactic API **
- pf_constr_of_global now returns a tactic instead of taking a continuation.
diff --git a/engine/namegen.ml b/engine/namegen.ml
index 3b979f206..5bd62273c 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -418,8 +418,7 @@ let use_h_based_elimination_names () =
open Goptions
let _ = declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "use of \"H\"-based proposition names in elimination tactics";
optkey = ["Standard";"Proposition";"Elimination";"Names"];
optread = (fun () -> !h_based_elimination_names);
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index ac7b38681..4e613f163 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -312,7 +312,7 @@ let import_option_value = function
| Interface.StringOptValue s -> Goptions.StringOptValue s
let export_option_state s = {
- Interface.opt_sync = s.Goptions.opt_sync;
+ Interface.opt_sync = true;
Interface.opt_depr = s.Goptions.opt_depr;
Interface.opt_name = s.Goptions.opt_name;
Interface.opt_value = export_option_value s.Goptions.opt_value;
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 692a0872b..4c29fc809 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -92,8 +92,7 @@ let record_print = ref true
let _ =
let open Goptions in
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "record printing";
optkey = ["Printing";"Records"];
optread = (fun () -> !record_print);
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 6d9cd4e3f..1fe63c19c 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -21,7 +21,7 @@ open Constrexpr_ops
let asymmetric_patterns = ref (false)
let _ = Goptions.declare_bool_option {
- Goptions.optsync = true; Goptions.optdepr = false;
+ Goptions.optdepr = false;
Goptions.optname = "no parameters in constructors";
Goptions.optkey = ["Asymmetric";"Patterns"];
Goptions.optread = (fun () -> !asymmetric_patterns);
diff --git a/library/goptions.ml b/library/goptions.ml
index c111113ca..9b4fc9985 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -24,7 +24,6 @@ type option_value =
(** Summary of an option status *)
type option_state = {
- opt_sync : bool;
opt_depr : bool;
opt_name : string;
opt_value : option_value;
@@ -62,7 +61,6 @@ module MakeTable =
val key : option_name
val title : string
val member_message : t -> bool -> std_ppcmds
- val synchronous : bool
end) ->
struct
type option_mark =
@@ -77,13 +75,9 @@ module MakeTable =
module MySet = Set.Make (struct type t = A.t let compare = A.compare end)
- let t =
- if A.synchronous
- then Summary.ref MySet.empty ~name:nick
- else ref MySet.empty
+ let t = Summary.ref MySet.empty ~name:nick
let (add_option,remove_option) =
- if A.synchronous then
let cache_options (_,(f,p)) = match f with
| GOadd -> t := MySet.add p !t
| GOrmv -> t := MySet.remove p !t in
@@ -103,9 +97,6 @@ module MakeTable =
in
((fun c -> Lib.add_anonymous_leaf (inGo (GOadd, c))),
(fun c -> Lib.add_anonymous_leaf (inGo (GOrmv, c))))
- else
- ((fun c -> t := MySet.add c !t),
- (fun c -> t := MySet.remove c !t))
let print_table table_name printer table =
Feedback.msg_notice
@@ -141,7 +132,6 @@ sig
val key : option_name
val title : string
val member_message : string -> bool -> std_ppcmds
- val synchronous : bool
end
module StringConvert = functor (A : StringConvertArg) ->
@@ -156,7 +146,6 @@ struct
let key = A.key
let title = A.title
let member_message = A.member_message
- let synchronous = A.synchronous
end
module MakeStringTable =
@@ -176,7 +165,6 @@ sig
val key : option_name
val title : string
val member_message : t -> bool -> std_ppcmds
- val synchronous : bool
end
module RefConvert = functor (A : RefConvertArg) ->
@@ -191,7 +179,6 @@ struct
let key = A.key
let title = A.title
let member_message = A.member_message
- let synchronous = A.synchronous
end
module MakeRefTable =
@@ -201,7 +188,6 @@ module MakeRefTable =
(* 2- Flags. *)
type 'a option_sig = {
- optsync : bool;
optdepr : bool;
optname : string;
optkey : option_name;
@@ -247,11 +233,10 @@ let get_locality = function
| None -> OptDefault
let declare_option cast uncast append ?(preprocess = fun x -> x)
- { optsync=sync; optdepr=depr; optname=name; optkey=key; optread=read; optwrite=write } =
+ { optdepr=depr; optname=name; optkey=key; optread=read; optwrite=write } =
check_key key;
let default = read() in
let change =
- if sync then
let _ = Summary.declare_summary (nickname key)
{ Summary.freeze_function = (fun _ -> read ());
Summary.unfreeze_function = write;
@@ -275,18 +260,12 @@ let declare_option cast uncast append ?(preprocess = fun x -> x)
discharge_function = discharge_options;
classify_function = classify_options } in
(fun l m v -> let v = preprocess v in Lib.add_anonymous_leaf (options (l, m, v)))
- else
- (fun _ m v ->
- let v = preprocess v in
- match m with
- | OptSet -> write v
- | OptAppend -> write (append (read ()) v))
in
let warn () = if depr then warn_deprecated_option key in
let cread () = cast (read ()) in
let cwrite l v = warn (); change l OptSet (uncast v) in
let cappend l v = warn (); change l OptAppend (uncast v) in
- value_tab := OptionMap.add key (name, depr, (sync,cread,cwrite,cappend)) !value_tab;
+ value_tab := OptionMap.add key (name, depr, (cread,cwrite,cappend)) !value_tab;
write
type 'a write_function = 'a -> unit
@@ -325,7 +304,7 @@ let set_option_value locality check_and_cast key v =
let opt = try Some (get_option key) with Not_found -> None in
match opt with
| None -> warn_unknown_option key
- | Some (name, depr, (_,read,write,append)) ->
+ | Some (name, depr, (read,write,append)) ->
write (get_locality locality) (check_and_cast v (read ()))
let bad_type_error () = error "Bad type of value for this option."
@@ -366,7 +345,7 @@ let set_string_option_append_value_gen locality key v =
let opt = try Some (get_option key) with Not_found -> None in
match opt with
| None -> warn_unknown_option key
- | Some (name, depr, (_,read,write,append)) ->
+ | Some (name, depr, (read,write,append)) ->
append (get_locality locality) (check_string_value v (read ()))
let set_int_option_value = set_int_option_value_gen None
@@ -387,7 +366,7 @@ let msg_option_value (name,v) =
(* | IdentValue r -> pr_global_env Id.Set.empty r *)
let print_option_value key =
- let (name, depr, (_,read,_,_)) = get_option key in
+ let (name, depr, (read,_,_)) = get_option key in
let s = read () in
match s with
| BoolValue b ->
@@ -397,9 +376,8 @@ let print_option_value key =
let get_tables () =
let tables = !value_tab in
- let fold key (name, depr, (sync,read,_,_)) accu =
+ let fold key (name, depr, (read,_,_)) accu =
let state = {
- opt_sync = sync;
opt_name = name;
opt_depr = depr;
opt_value = read ();
@@ -416,15 +394,8 @@ let print_tables () =
in
str "Synchronous options:" ++ fnl () ++
OptionMap.fold
- (fun key (name, depr, (sync,read,_,_)) p ->
- if sync then p ++ print_option key name (read ()) depr
- else p)
- !value_tab (mt ()) ++
- str "Asynchronous options:" ++ fnl () ++
- OptionMap.fold
- (fun key (name, depr, (sync,read,_,_)) p ->
- if sync then p
- else p ++ print_option key name (read ()) depr)
+ (fun key (name, depr, (read,_,_)) p ->
+ p ++ print_option key name (read ()) depr)
!value_tab (mt ()) ++
str "Tables:" ++ fnl () ++
List.fold_right
diff --git a/library/goptions.mli b/library/goptions.mli
index 3b3651f39..f612c4e36 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -40,8 +40,8 @@
Unset Tata Tutu Titi.
Print Table Tata Tutu Titi. (** synonym: Test Table Tata Tutu Titi. *)
- The created table/option may be declared synchronous or not
- (synchronous = consistent with the resetting commands) *)
+ All options are synchronized with the document.
+*)
open Pp
open Libnames
@@ -65,7 +65,6 @@ module MakeStringTable :
val key : option_name
val title : string
val member_message : string -> bool -> std_ppcmds
- val synchronous : bool
end) ->
sig
val active : string -> bool
@@ -93,7 +92,6 @@ module MakeRefTable :
val key : option_name
val title : string
val member_message : t -> bool -> std_ppcmds
- val synchronous : bool
end) ->
sig
val active : A.t -> bool
@@ -108,8 +106,6 @@ module MakeRefTable :
used when printing the option value (command "Print Toto Titi." *)
type 'a option_sig = {
- optsync : bool;
- (** whether the option is synchronous w.r.t to the section/module system. *)
optdepr : bool;
(** whether the option is DEPRECATED *)
optname : string;
@@ -120,8 +116,6 @@ type 'a option_sig = {
optwrite : 'a -> unit
}
-(** When an option is declared synchronous ([optsync] is [true]), the output is
- a synchronous write function. Otherwise it is [optwrite] *)
(** The [preprocess] function is triggered before setting the option. It can be
used to emit a warning on certain values, and clean-up the final value. *)
@@ -177,7 +171,6 @@ type option_value =
(** Summary of an option status *)
type option_state = {
- opt_sync : bool;
opt_depr : bool;
opt_name : string;
opt_value : option_value;
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;
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index bd7350dc4..782552583 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -177,7 +177,7 @@ let cofixp_reducible flgs _ stk =
let debug_cbv = ref false
let _ = Goptions.declare_bool_option {
- Goptions.optsync = true; Goptions.optdepr = false;
+ Goptions.optdepr = false;
Goptions.optname = "cbv visited constants display";
Goptions.optkey = ["Debug";"Cbv"];
Goptions.optread = (fun () -> !debug_cbv);
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 32da81f96..9a973cff5 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -428,8 +428,7 @@ let automatically_import_coercions = ref false
open Goptions
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "automatic import of coercions";
optkey = ["Automatic";"Coercions";"Import"];
optread = (fun () -> !automatically_import_coercions);
@@ -556,7 +555,6 @@ module CoercionPrinting =
let member_message x b =
str "Explicit printing of coercion " ++ printer x ++
str (if b then " is set" else " is unset")
- let synchronous = true
end
module PrintingCoercion = Goptions.MakeRefTable(CoercionPrinting)
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 98a00f433..3ef17912f 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -33,14 +33,13 @@ open Globnames
let use_typeclasses_for_conversion = ref true
let _ =
- Goptions.declare_bool_option
- { Goptions.optsync = true;
- optdepr = false;
+ Goptions.(declare_bool_option
+ { optdepr = false;
optname = "use typeclass resolution during conversion";
optkey = ["Typeclass"; "Resolution"; "For"; "Conversion"];
optread = (fun () -> !use_typeclasses_for_conversion);
optwrite = (fun b -> use_typeclasses_for_conversion := b) }
-
+ )
(* Typing operations dealing with coercions *)
exception NoCoercion
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 92359420e..752819aa3 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -133,8 +133,7 @@ let wildcard_value = ref true
let force_wildcard () = !wildcard_value
let _ = declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "forced wildcard";
optkey = ["Printing";"Wildcard"];
optread = force_wildcard;
@@ -144,8 +143,7 @@ let synth_type_value = ref true
let synthetize_type () = !synth_type_value
let _ = declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "pattern matching return type synthesizability";
optkey = ["Printing";"Synth"];
optread = synthetize_type;
@@ -155,8 +153,7 @@ let reverse_matching_value = ref true
let reverse_matching () = !reverse_matching_value
let _ = declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "pattern-matching reversibility";
optkey = ["Printing";"Matching"];
optread = reverse_matching;
@@ -166,8 +163,7 @@ let print_primproj_params_value = ref false
let print_primproj_params () = !print_primproj_params_value
let _ = declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "printing of primitive projection parameters";
optkey = ["Printing";"Primitive";"Projection";"Parameters"];
optread = print_primproj_params;
@@ -177,8 +173,7 @@ let print_primproj_compatibility_value = ref false
let print_primproj_compatibility () = !print_primproj_compatibility_value
let _ = declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "backwards-compatible printing of primitive projections";
optkey = ["Printing";"Primitive";"Projection";"Compatibility"];
optread = print_primproj_compatibility;
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 6fcbaa8ef..42aaf3a22 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -34,7 +34,7 @@ type unify_fun = transparent_state ->
let debug_unification = ref (false)
let _ = Goptions.declare_bool_option {
- Goptions.optsync = true; Goptions.optdepr = false;
+ Goptions.optdepr = false;
Goptions.optname =
"Print states sent to Evarconv unification";
Goptions.optkey = ["Debug";"Unification"];
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 53df5aa4a..75fda97b8 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -175,8 +175,7 @@ let is_strict_universe_declarations () = !strict_universe_declarations
let _ =
Goptions.(declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "strict universe declaration";
optkey = ["Strict";"Universe";"Declaration"];
optread = is_strict_universe_declarations;
@@ -184,8 +183,7 @@ let _ =
let _ =
Goptions.(declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "minimization to Set";
optkey = ["Universe";"Minimization";"ToSet"];
optread = Universes.is_set_minimization;
diff --git a/pretyping/program.ml b/pretyping/program.ml
index 42acc5705..de485dbe8 100644
--- a/pretyping/program.ml
+++ b/pretyping/program.ml
@@ -87,8 +87,7 @@ open Goptions
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "preferred transparency of Program obligations";
optkey = ["Transparent";"Obligations"];
optread = get_proofs_transparency;
@@ -96,8 +95,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "program cases";
optkey = ["Program";"Cases"];
optread = (fun () -> !program_cases);
@@ -105,8 +103,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "program generalized coercion";
optkey = ["Program";"Generalized";"Coercion"];
optread = (fun () -> !program_generalized_coercion);
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 52f424f75..117ed338e 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -29,7 +29,7 @@ exception Elimconst
let refolding_in_reduction = ref false
let _ = Goptions.declare_bool_option {
- Goptions.optsync = true; Goptions.optdepr = false;
+ Goptions.optdepr = false;
Goptions.optname =
"Perform refolding of fixpoints/constants like cbn during reductions";
Goptions.optkey = ["Refolding";"Reduction"];
@@ -811,7 +811,7 @@ let fix_recarg ((recindices,bodynum),_) stack =
let debug_RAKAM = ref (false)
let _ = Goptions.declare_bool_option {
- Goptions.optsync = true; Goptions.optdepr = false;
+ Goptions.optdepr = false;
Goptions.optname =
"Print states of the Reductionops abstract machine";
Goptions.optkey = ["Debug";"RAKAM"];
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 93c71e6ea..919e95a8e 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -30,8 +30,7 @@ open Goptions
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "check that typeclasses proof search returns unique solutions";
optkey = ["Typeclasses";"Unique";"Solutions"];
optread = get_typeclasses_unique_solutions;
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 74fbd2a85..cac6c5057 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -45,7 +45,7 @@ module NamedDecl = Context.Named.Declaration
let keyed_unification = ref (false)
let _ = Goptions.declare_bool_option {
- Goptions.optsync = true; Goptions.optdepr = false;
+ Goptions.optdepr = false;
Goptions.optname = "Unification is keyed";
Goptions.optkey = ["Keyed";"Unification"];
Goptions.optread = (fun () -> !keyed_unification);
@@ -56,7 +56,7 @@ let is_keyed_unification () = !keyed_unification
let debug_unification = ref (false)
let _ = Goptions.declare_bool_option {
- Goptions.optsync = true; Goptions.optdepr = false;
+ Goptions.optdepr = false;
Goptions.optname =
"Print states sent to tactic unification";
Goptions.optkey = ["Debug";"Tactic";"Unification"];
@@ -257,8 +257,7 @@ let global_pattern_unification_flag = ref true
open Goptions
let _ =
declare_bool_option
- { optsync = true;
- optdepr = true;
+ { optdepr = true;
optname = "pattern-unification for existential variables in tactics";
optkey = ["Tactic";"Evars";"Pattern";"Unification"];
optread = (fun () -> !global_pattern_unification_flag);
@@ -269,8 +268,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "pattern-unification for existential variables in tactics";
optkey = ["Tactic";"Pattern";"Unification"];
optread = (fun () -> !global_pattern_unification_flag);
diff --git a/printing/printer.ml b/printing/printer.ml
index 40a3660b3..d4f7afb38 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -44,8 +44,7 @@ let should_gname() = !enable_goal_names_printing
let _ =
let open Goptions in
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "printing of unfocused goal";
optkey = ["Printing";"Unfocused"];
optread = (fun () -> !enable_unfocused_goal_printing);
@@ -56,8 +55,7 @@ let _ =
let _ =
let open Goptions in
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "printing of goal tags";
optkey = ["Printing";"Goal";"Tags"];
optread = (fun () -> !enable_goal_tags_printing);
@@ -67,8 +65,7 @@ let _ =
let _ =
let open Goptions in
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "printing of goal names";
optkey = ["Printing";"Goal";"Names"];
optread = (fun () -> !enable_goal_names_printing);
@@ -449,8 +446,7 @@ let print_hyps_limit = ref (None : int option)
let _ =
let open Goptions in
declare_int_option
- { optsync = false;
- optdepr = false;
+ { optdepr = false;
optname = "the hypotheses limit";
optkey = ["Hyps";"Limit"];
optread = (fun () -> !print_hyps_limit);
@@ -635,8 +631,7 @@ let should_print_dependent_evars = ref false
let _ =
let open Goptions in
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "Printing Dependent Evars Line";
optkey = ["Printing";"Dependent";"Evars";"Line"];
optread = (fun () -> !should_print_dependent_evars);
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 6f4b162d7..c4affd4ac 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -42,8 +42,7 @@ let short = ref false
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "short module printing";
optkey = ["Short";"Module";"Printing"];
optread = (fun () -> !short) ;
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 7e8ed31d1..92b4e788a 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -15,7 +15,7 @@ open Evd
let use_unification_heuristics_ref = ref true
let _ = Goptions.declare_bool_option {
- Goptions.optsync = true; Goptions.optdepr = false;
+ Goptions.optdepr = false;
Goptions.optname = "Solve unification constraints at every \".\"";
Goptions.optkey = ["Solve";"Unification";"Constraints"];
Goptions.optread = (fun () -> !use_unification_heuristics_ref);
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 2396db868..95aee72cb 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -52,8 +52,7 @@ let get_default_proof_mode_name () =
(CEphemeron.default !default_proof_mode standard).name
let _ =
- Goptions.declare_string_option {Goptions.
- optsync = true ;
+ Goptions.(declare_string_option {
optdepr = false;
optname = "default proof mode" ;
optkey = ["Default";"Proof";"Mode"] ;
@@ -63,7 +62,7 @@ let _ =
optwrite = begin fun n ->
default_proof_mode := find_proof_mode n
end
- }
+ })
(*** Proof Global Environment ***)
@@ -268,8 +267,7 @@ let get_universe_binders () = (cur_pstate ()).universe_binders
let proof_using_auto_clear = ref false
let _ = Goptions.declare_bool_option
- { Goptions.optsync = true;
- Goptions.optdepr = false;
+ { Goptions.optdepr = false;
Goptions.optname = "Proof using Clear Unused";
Goptions.optkey = ["Proof";"Using";"Clear";"Unused"];
Goptions.optread = (fun () -> !proof_using_auto_clear);
@@ -628,8 +626,7 @@ module Bullet = struct
let current_behavior = ref Strict.strict
let _ =
- Goptions.declare_string_option {Goptions.
- optsync = true;
+ Goptions.(declare_string_option {
optdepr = false;
optname = "bullet behavior";
optkey = ["Bullet";"Behavior"];
@@ -642,7 +639,7 @@ module Bullet = struct
with Not_found ->
CErrors.error ("Unknown bullet behavior: \"" ^ n ^ "\".")
end
- }
+ })
let put p b =
(!current_behavior).put p b
@@ -696,9 +693,7 @@ let parse_goal_selector = function
end
let _ =
- Goptions.declare_string_option {Goptions.
- optsync = true ;
- optdepr = false;
+ Goptions.(declare_string_option{optdepr = false;
optname = "default goal selector" ;
optkey = ["Default";"Goal";"Selector"] ;
optread = begin fun () ->
@@ -708,7 +703,7 @@ let _ =
optwrite = begin fun n ->
default_goal_selector := parse_goal_selector n
end
- }
+ })
module V82 = struct
diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml
index f0854e9aa..f701f7cfe 100644
--- a/proofs/proof_using.ml
+++ b/proofs/proof_using.ml
@@ -144,8 +144,7 @@ let value = ref false
let _ =
Goptions.declare_bool_option
- { Goptions.optsync = true;
- Goptions.optdepr = false;
+ { Goptions.optdepr = false;
Goptions.optname = "suggest Proof using";
Goptions.optkey = ["Suggest";"Proof";"Using"];
Goptions.optread = (fun () -> !value);
@@ -159,8 +158,7 @@ let value = ref None
let _ =
Goptions.declare_stringopt_option
- { Goptions.optsync = true;
- Goptions.optdepr = false;
+ { Goptions.optdepr = false;
Goptions.optname = "default value for Proof using";
Goptions.optkey = ["Default";"Proof";"Using"];
Goptions.optread = (fun () -> !value);
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index cb3538422..7cd526843 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -52,7 +52,7 @@ let strong_cbn flags =
let simplIsCbn = ref (false)
let _ = Goptions.declare_bool_option {
- Goptions.optsync = true; Goptions.optdepr = false;
+ Goptions.optdepr = false;
Goptions.optname =
"Plug the simpl tactic to the new cbn mechanism";
Goptions.optkey = ["SimplIsCbn"];
diff --git a/tactics/auto.ml b/tactics/auto.ml
index c2d12ebd0..b76c0a96a 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -174,8 +174,7 @@ let global_info_auto = ref false
let add_option ls refe =
let _ = Goptions.declare_bool_option
- { Goptions.optsync = true;
- Goptions.optdepr = false;
+ { Goptions.optdepr = false;
Goptions.optname = String.concat " " ls;
Goptions.optkey = ls;
Goptions.optread = (fun () -> !refe);
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 05eb0a976..918371d55 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -92,8 +92,7 @@ open Goptions
let _ =
declare_bool_option
- { optsync = true;
- optdepr = true;
+ { optdepr = true;
optname = "do typeclass search modulo eta conversion";
optkey = ["Typeclasses";"Modulo";"Eta"];
optread = get_typeclasses_modulo_eta;
@@ -101,8 +100,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "do typeclass search avoiding eta-expansions " ^
" in proof terms (expensive)";
optkey = ["Typeclasses";"Limit";"Intros"];
@@ -111,8 +109,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "during typeclass resolution, solve instances according to their dependency order";
optkey = ["Typeclasses";"Dependency";"Order"];
optread = get_typeclasses_dependency_order;
@@ -120,8 +117,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "use iterative deepening strategy";
optkey = ["Typeclasses";"Iterative";"Deepening"];
optread = get_typeclasses_iterative_deepening;
@@ -129,8 +125,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "compat";
optkey = ["Typeclasses";"Legacy";"Resolution"];
optread = get_typeclasses_legacy_resolution;
@@ -138,8 +133,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "compat";
optkey = ["Typeclasses";"Filtered";"Unification"];
optread = get_typeclasses_filtered_unification;
@@ -147,8 +141,7 @@ let _ =
let set_typeclasses_debug =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "debug output for typeclasses proof search";
optkey = ["Typeclasses";"Debug"];
optread = get_typeclasses_debug;
@@ -156,8 +149,7 @@ let set_typeclasses_debug =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "debug output for typeclasses proof search";
optkey = ["Debug";"Typeclasses"];
optread = get_typeclasses_debug;
@@ -165,8 +157,7 @@ let _ =
let _ =
declare_int_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "verbosity of debug output for typeclasses proof search";
optkey = ["Typeclasses";"Debug";"Verbosity"];
optread = get_typeclasses_verbose;
@@ -174,8 +165,7 @@ let _ =
let set_typeclasses_depth =
declare_int_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "depth for typeclasses proof search";
optkey = ["Typeclasses";"Depth"];
optread = get_typeclasses_depth;
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 8d1e0e507..e87368dec 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -331,8 +331,7 @@ let global_info_eauto = ref false
let _ =
Goptions.declare_bool_option
- { Goptions.optsync = true;
- Goptions.optdepr = false;
+ { Goptions.optdepr = false;
Goptions.optname = "Debug Eauto";
Goptions.optkey = ["Debug";"Eauto"];
Goptions.optread = (fun () -> !global_debug_eauto);
@@ -340,8 +339,7 @@ let _ =
let _ =
Goptions.declare_bool_option
- { Goptions.optsync = true;
- Goptions.optdepr = false;
+ { Goptions.optdepr = false;
Goptions.optname = "Info Eauto";
Goptions.optkey = ["Info";"Eauto"];
Goptions.optread = (fun () -> !global_info_eauto);
diff --git a/tactics/equality.ml b/tactics/equality.ml
index b0f27663e..70d6fe90c 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -57,8 +57,7 @@ let discr_do_intro () =
open Goptions
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "automatic introduction of hypotheses by discriminate";
optkey = ["Discriminate";"Introduction"];
optread = (fun () -> !discriminate_introduction);
@@ -72,8 +71,7 @@ let use_injection_pattern_l2r_order () =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "injection left-to-right pattern order and clear by default when with introduction pattern";
optkey = ["Injection";"L2R";"Pattern";"Order"];
optread = (fun () -> !injection_pattern_l2r_order) ;
@@ -87,8 +85,7 @@ let use_injection_in_context () =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "injection in context";
optkey = ["Structural";"Injection"];
optread = (fun () -> !injection_in_context) ;
@@ -729,8 +726,7 @@ let keep_proof_equalities_for_injection = ref false
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "injection on prop arguments";
optkey = ["Keep";"Proof";"Equalities"];
optread = (fun () -> !keep_proof_equalities_for_injection) ;
@@ -1680,8 +1676,7 @@ let regular_subst_tactic = ref true
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "more regular behavior of tactic subst";
optkey = ["Regular";"Subst";"Tactic"];
optread = (fun () -> !regular_subst_tactic);
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 61bc3d284..0c796b886 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -171,8 +171,7 @@ let write_warn_hint = function
let _ =
Goptions.declare_string_option
- { Goptions.optsync = true;
- Goptions.optdepr = false;
+ { Goptions.optdepr = false;
Goptions.optname = "behavior of non-imported hints";
Goptions.optkey = ["Loose"; "Hint"; "Behavior"];
Goptions.optread = read_warn_hint;
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 11c281985..1975eed9d 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -70,8 +70,7 @@ let use_dependent_propositions_elimination () =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "dependent-propositions-elimination tactic";
optkey = ["Dependent";"Propositions";"Elimination"];
optread = (fun () -> !dependent_propositions_elimination) ;
@@ -79,8 +78,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "trigger bugged context matching compatibility";
optkey = ["Tactic";"Compat";"Context"];
optread = (fun () -> !Flags.tactic_context_compat) ;
@@ -88,7 +86,7 @@ let _ =
let apply_solve_class_goals = ref (false)
let _ = Goptions.declare_bool_option {
- Goptions.optsync = true; Goptions.optdepr = true;
+ Goptions.optdepr = true;
Goptions.optname =
"Perform typeclass resolution on apply-generated subgoals.";
Goptions.optkey = ["Typeclass";"Resolution";"After";"Apply"];
@@ -102,8 +100,7 @@ let use_clear_hyp_by_default () = !clear_hyp_by_default
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "default clearing of hypotheses after use";
optkey = ["Default";"Clearing";"Used";"Hypotheses"];
optread = (fun () -> !clear_hyp_by_default) ;
@@ -119,8 +116,7 @@ let accept_universal_lemma_under_conjunctions () =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "trivial unification in tactics applying under conjunctions";
optkey = ["Universal";"Lemma";"Under";"Conjunction"];
optread = (fun () -> !universal_lemma_under_conjunctions) ;
@@ -132,8 +128,7 @@ let shrink_abstract = ref true
let _ =
declare_bool_option
- { optsync = true;
- optdepr = true;
+ { optdepr = true;
optname = "shrinking of abstracted proofs";
optkey = ["Shrink"; "Abstract"];
optread = (fun () -> !shrink_abstract) ;
@@ -153,8 +148,7 @@ let use_bracketing_last_or_and_intro_pattern () =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "bracketing last or-and introduction pattern";
optkey = ["Bracketing";"Last";"Introduction";"Pattern"];
optread = (fun () -> !bracketing_last_or_and_intro_pattern);
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 884959c57..5843da31e 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -32,7 +32,6 @@ open Entries
let refine_instance = ref true
let _ = Goptions.declare_bool_option {
- Goptions.optsync = true;
Goptions.optdepr = false;
Goptions.optname = "definition of instances by refining";
Goptions.optkey = ["Refine";"Instance";"Mode"];
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 2367177e2..b21e80bef 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -45,8 +45,7 @@ open Context.Rel.Declaration
let elim_flag = ref true
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "automatic declaration of induction schemes";
optkey = ["Elimination";"Schemes"];
optread = (fun () -> !elim_flag) ;
@@ -55,16 +54,14 @@ let _ =
let bifinite_elim_flag = ref false
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "automatic declaration of induction schemes for non-recursive types";
optkey = ["Nonrecursive";"Elimination";"Schemes"];
optread = (fun () -> !bifinite_elim_flag) ;
optwrite = (fun b -> bifinite_elim_flag := b) }
let _ =
declare_bool_option
- { optsync = true;
- optdepr = true; (* compatibility 2014-09-03*)
+ { optdepr = true; (* compatibility 2014-09-03*)
optname = "automatic declaration of induction schemes for non-recursive types";
optkey = ["Record";"Elimination";"Schemes"];
optread = (fun () -> !bifinite_elim_flag) ;
@@ -73,8 +70,7 @@ let _ =
let case_flag = ref false
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "automatic declaration of case analysis schemes";
optkey = ["Case";"Analysis";"Schemes"];
optread = (fun () -> !case_flag) ;
@@ -83,16 +79,14 @@ let _ =
let eq_flag = ref false
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "automatic declaration of boolean equality";
optkey = ["Boolean";"Equality";"Schemes"];
optread = (fun () -> !eq_flag) ;
optwrite = (fun b -> eq_flag := b) }
let _ = (* compatibility *)
declare_bool_option
- { optsync = true;
- optdepr = true;
+ { optdepr = true;
optname = "automatic declaration of boolean equality";
optkey = ["Equality";"Scheme"];
optread = (fun () -> !eq_flag) ;
@@ -103,8 +97,7 @@ let is_eq_flag () = !eq_flag && Flags.version_strictly_greater Flags.V8_2
let eq_dec_flag = ref false
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "automatic declaration of decidable equality";
optkey = ["Decidable";"Equality";"Schemes"];
optread = (fun () -> !eq_dec_flag) ;
@@ -113,8 +106,7 @@ let _ =
let rewriting_flag = ref false
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname ="automatic declaration of rewriting schemes for equality types";
optkey = ["Rewriting";"Schemes"];
optread = (fun () -> !rewriting_flag) ;
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 8dc444a43..c67a3302f 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -465,8 +465,7 @@ let keep_admitted_vars = ref true
let _ =
let open Goptions in
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "keep section variables in admitted proofs";
optkey = ["Keep"; "Admitted"; "Variables"];
optread = (fun () -> !keep_admitted_vars);
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 331b025f0..64c156030 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -340,8 +340,7 @@ let get_hide_obligations () = !hide_obligations
open Goptions
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "Hidding of Program obligations";
optkey = ["Hide";"Obligations"];
optread = get_hide_obligations;
@@ -354,8 +353,7 @@ let get_shrink_obligations () = !shrink_obligations
let _ =
declare_bool_option
- { optsync = true;
- optdepr = true;
+ { optdepr = true;
optname = "Shrinking of Program obligations";
optkey = ["Shrink";"Obligations"];
optread = get_shrink_obligations;
diff --git a/vernac/record.ml b/vernac/record.ml
index e33e1f8cd..10207d0e0 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -35,8 +35,7 @@ module RelDecl = Context.Rel.Declaration
let primitive_flag = ref false
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "use of primitive projections";
optkey = ["Primitive";"Projections"];
optread = (fun () -> !primitive_flag) ;
@@ -45,8 +44,7 @@ let _ =
let typeclasses_strict = ref false
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "strict typeclass resolution";
optkey = ["Typeclasses";"Strict";"Resolution"];
optread = (fun () -> !typeclasses_strict);
@@ -55,8 +53,7 @@ let _ =
let typeclasses_unique = ref false
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "unique typeclass instances";
optkey = ["Typeclasses";"Unique";"Instances"];
optread = (fun () -> !typeclasses_unique);
diff --git a/vernac/search.ml b/vernac/search.ml
index 5b6e9a9c3..916015800 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -40,7 +40,6 @@ module SearchBlacklist =
let title = "Current search blacklist : "
let member_message s b =
str "Search blacklist does " ++ (if b then mt () else str "not ") ++ str "include " ++ str s
- let synchronous = true
end)
(* The functions iter_constructors and iter_declarations implement the behavior
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index dc3bf6ba7..f75e04383 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1228,8 +1228,7 @@ let vernac_generalizable locality =
let _ =
declare_bool_option
- { optsync = false;
- optdepr = false;
+ { optdepr = false;
optname = "silent";
optkey = ["Silent"];
optread = (fun () -> !Flags.quiet);
@@ -1237,8 +1236,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "implicit arguments";
optkey = ["Implicit";"Arguments"];
optread = Impargs.is_implicit_args;
@@ -1246,8 +1244,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "strict implicit arguments";
optkey = ["Strict";"Implicit"];
optread = Impargs.is_strict_implicit_args;
@@ -1255,8 +1252,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "strong strict implicit arguments";
optkey = ["Strongly";"Strict";"Implicit"];
optread = Impargs.is_strongly_strict_implicit_args;
@@ -1264,8 +1260,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "contextual implicit arguments";
optkey = ["Contextual";"Implicit"];
optread = Impargs.is_contextual_implicit_args;
@@ -1273,8 +1268,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "implicit status of reversible patterns";
optkey = ["Reversible";"Pattern";"Implicit"];
optread = Impargs.is_reversible_pattern_implicit_args;
@@ -1282,8 +1276,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "maximal insertion of implicit";
optkey = ["Maximal";"Implicit";"Insertion"];
optread = Impargs.is_maximal_implicit_args;
@@ -1291,8 +1284,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "automatic introduction of variables";
optkey = ["Automatic";"Introduction"];
optread = Flags.is_auto_intros;
@@ -1300,8 +1292,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "coercion printing";
optkey = ["Printing";"Coercions"];
optread = (fun () -> !Constrextern.print_coercions);
@@ -1309,8 +1300,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "printing of existential variable instances";
optkey = ["Printing";"Existential";"Instances"];
optread = (fun () -> !Detyping.print_evar_arguments);
@@ -1318,8 +1308,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "implicit arguments printing";
optkey = ["Printing";"Implicit"];
optread = (fun () -> !Constrextern.print_implicits);
@@ -1327,8 +1316,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "implicit arguments defensive printing";
optkey = ["Printing";"Implicit";"Defensive"];
optread = (fun () -> !Constrextern.print_implicits_defensive);
@@ -1336,8 +1324,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "projection printing using dot notation";
optkey = ["Printing";"Projections"];
optread = (fun () -> !Constrextern.print_projections);
@@ -1345,8 +1332,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "notations printing";
optkey = ["Printing";"Notations"];
optread = (fun () -> not !Constrextern.print_no_symbol);
@@ -1354,8 +1340,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "raw printing";
optkey = ["Printing";"All"];
optread = (fun () -> !Flags.raw_print);
@@ -1363,8 +1348,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "use of the program extension";
optkey = ["Program";"Mode"];
optread = (fun () -> !Flags.program_mode);
@@ -1372,8 +1356,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "universe polymorphism";
optkey = ["Universe"; "Polymorphism"];
optread = Flags.is_universe_polymorphism;
@@ -1381,8 +1364,7 @@ let _ =
let _ =
declare_int_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "the level of inlining during functor application";
optkey = ["Inline";"Level"];
optread = (fun () -> Some (Flags.get_inline_level ()));
@@ -1392,8 +1374,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "kernel term sharing";
optkey = ["Kernel"; "Term"; "Sharing"];
optread = (fun () -> !CClosure.share);
@@ -1404,8 +1385,7 @@ let _ =
let _ =
declare_int_option
- { optsync = false;
- optdepr = true;
+ { optdepr = true;
optname = "the undo limit (OBSOLETE)";
optkey = ["Undo"];
optread = (fun _ -> None);
@@ -1413,8 +1393,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "display compact goal contexts";
optkey = ["Printing";"Compact";"Contexts"];
optread = (fun () -> Printer.get_compact_context());
@@ -1422,8 +1401,7 @@ let _ =
let _ =
declare_int_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "the printing depth";
optkey = ["Printing";"Depth"];
optread = Topfmt.get_depth_boxes;
@@ -1431,8 +1409,7 @@ let _ =
let _ =
declare_int_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "the printing width";
optkey = ["Printing";"Width"];
optread = Topfmt.get_margin;
@@ -1440,8 +1417,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "printing of universes";
optkey = ["Printing";"Universes"];
optread = (fun () -> !Constrextern.print_universes);
@@ -1449,8 +1425,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "dumping bytecode after compilation";
optkey = ["Dump";"Bytecode"];
optread = Flags.get_dump_bytecode;
@@ -1458,8 +1433,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "explicitly parsing implicit arguments";
optkey = ["Parsing";"Explicit"];
optread = (fun () -> !Constrintern.parsing_explicit);
@@ -1467,8 +1441,7 @@ let _ =
let _ =
declare_string_option ~preprocess:CWarnings.normalize_flags_string
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "warnings display";
optkey = ["Warnings"];
optread = CWarnings.get_flags;
@@ -1739,8 +1712,7 @@ let search_output_name_only = ref false
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "output-name-only search";
optkey = ["Search";"Output";"Name";"Only"];
optread = (fun () -> !search_output_name_only);
@@ -2137,8 +2109,7 @@ let default_timeout = ref None
let _ =
Goptions.declare_int_option
- { Goptions.optsync = true;
- Goptions.optdepr = false;
+ { Goptions.optdepr = false;
Goptions.optname = "the default timeout";
Goptions.optkey = ["Default";"Timeout"];
Goptions.optread = (fun () -> !default_timeout);